Theorem trnsp-P1.15a 76

Description: Transposition Variant A.

Assertion

Ref	Expression
trnsp-P1.15a	⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑))

Proof of Theorem trnsp-P1.15a

Step	Hyp	Ref	Expression
1		dneg-P1.13a 71	. . 3 ⊢ (¬ ¬ 𝜑 → 𝜑)
2	1	imsubl-P1.7b.SH 55	. 2 ⊢ ((𝜑 → ¬ 𝜓) → (¬ ¬ 𝜑 → ¬ 𝜓))
3		ax-L3 13	. 2 ⊢ ((¬ ¬ 𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑))
4	2, 3	syl-P1.2 34	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:  trnsp-P1.15a.SH  77  trnsp-P1.15c  80  pfbycont-P1.16  86