Theorem frege52aid 38152

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 205. Part of Axiom 52 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)

Assertion

Ref	Expression
frege52aid	|- ( ( ph <-> ps ) -> ( ph -> ps ) )

Proof of Theorem frege52aid

Step	Hyp	Ref	Expression
1		ax-frege52a 38151	. 2 |- ( ( ph <-> ps ) -> (if- ( ph , T. , F. ) -> if- ( ps , T. , F. ) ) )
2		ifpid2 37815	. 2 |- ( ph <-> if- ( ph , T. , F. ) )
3		ifpid2 37815	. 2 |- ( ps <-> if- ( ps , T. , F. ) )
4	1, 2, 3	3imtr4g 285	1 |- ( ( ph <-> ps ) -> ( ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 196  if-wif 1012   T. wtru 1484   F. wfal 1488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-frege52a 38151

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ifp 1013  df-tru 1486  df-fal 1489

This theorem is referenced by:  frege53aid  38153  frege57aid  38166  frege75  38232  frege89  38246  frege105  38262