Theorem mbicmb-P2.1c 103

Description: Motivation for ↔ Definition, Part C.

Hypotheses

Ref	Expression
mbicmb-P2.1c.1	⊢ (𝜑 → 𝜓)
mbicmb-P2.1c.2	⊢ (𝜓 → 𝜑)

Assertion

Ref	Expression
mbicmb-P2.1c	⊢ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))

Proof of Theorem mbicmb-P2.1c

Step	Hyp	Ref	Expression
1		mbicmb-P2.1c.1	. 2 ⊢ (𝜑 → 𝜓)
2		mbicmb-P2.1c.2	. 2 ⊢ (𝜓 → 𝜑)
3	1, 2	cmb-L2.3.2SH 100	1 ⊢ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))

Syntax hints:  ¬ wff-neg 9   → wff-imp 10

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-L3 13  ax-MP 14

This theorem is referenced by: (None)