Theorem frege52aid

Description: The case when the content of ph is identical with the content of ps and in which ph is affirmed and ps is denied does not take place. Identical to biimp . Part of Axiom 52 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	frege52aid	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜑 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		ax-frege52a	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( if- ( 𝜑 , ⊤ , ⊥ ) → if- ( 𝜓 , ⊤ , ⊥ ) ) )
2		ifpid2	⊢ ( 𝜑 ↔ if- ( 𝜑 , ⊤ , ⊥ ) )
3		ifpid2	⊢ ( 𝜓 ↔ if- ( 𝜓 , ⊤ , ⊥ ) )
4	1 2 3	3imtr4g	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜑 → 𝜓 ) )