Theorem frege53a 38154

Description: Lemma for frege55a 38162. Proposition 53 of [Frege1879] p. 50. (Contributed by RP, 24-Dec-2019.) (Proof modification is discouraged.)

Assertion

Ref	Expression
frege53a	|- (if- ( ph , th , ch ) -> ( ( ph <-> ps ) -> if- ( ps , th , ch ) ) )

Proof of Theorem frege53a

Step	Hyp	Ref	Expression
1		ax-frege52a 38151	. 2 |- ( ( ph <-> ps ) -> (if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) )
2		ax-frege8 38103	. 2 |- ( ( ( ph <-> ps ) -> (if- ( ph , th , ch ) -> if- ( ps , th , ch ) ) ) -> (if- ( ph , th , ch ) -> ( ( ph <-> ps ) -> if- ( ps , th , ch ) ) ) )
3	1, 2	ax-mp 5	1 |- (if- ( ph , th , ch ) -> ( ( ph <-> ps ) -> if- ( ps , th , ch ) ) )

Syntax hints:   -> wi 4   <-> wb 196  if-wif 1012

This theorem was proved from axioms:  ax-mp 5  ax-frege8 38103  ax-frege52a 38151

This theorem is referenced by:  frege55a  38162