Metamath Proof Explorer

Theorem frege55a

Description: Proposition 55 of Frege1879 p. 50. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

Ref Expression
Assertion frege55a 
|- ( ( ph <-> ps ) -> if- ( ps , ph , -. ph ) )

Proof

Step Hyp Ref Expression
1 frege54cor1a 
 |-  if- ( ph , ph , -. ph )
2 frege53a 
 |-  ( if- ( ph , ph , -. ph ) -> ( ( ph <-> ps ) -> if- ( ps , ph , -. ph ) ) )
3 1 2 ax-mp 
 |-  ( ( ph <-> ps ) -> if- ( ps , ph , -. ph ) )