Metamath Proof Explorer

Theorem axfrege58a

Description: Identical to anifp . Justification for ax-frege58a . (Contributed by RP, 28-Mar-2020)

Ref Expression
Assertion axfrege58a 
|- ( ( ps /\ ch ) -> if- ( ph , ps , ch ) )

Proof

Step Hyp Ref Expression
1 anifp 
 |-  ( ( ps /\ ch ) -> if- ( ph , ps , ch ) )