Theorem con1b

Description: Contraposition. Bidirectional version of con1 . (Contributed by NM, 3-Jan-1993)

	Ref	Expression
Assertion	con1b	⊢ ( ( ¬ 𝜑 → 𝜓 ) ↔ ( ¬ 𝜓 → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		con1	⊢ ( ( ¬ 𝜑 → 𝜓 ) → ( ¬ 𝜓 → 𝜑 ) )
2		con1	⊢ ( ( ¬ 𝜓 → 𝜑 ) → ( ¬ 𝜑 → 𝜓 ) )
3	1 2	impbii	⊢ ( ( ¬ 𝜑 → 𝜓 ) ↔ ( ¬ 𝜓 → 𝜑 ) )