Theorem axfrege58a

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

	Ref	Expression
Assertion	axfrege58a	⊢ ( ( 𝜓 ∧ 𝜒 ) → if- ( 𝜑 , 𝜓 , 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		anifp	⊢ ( ( 𝜓 ∧ 𝜒 ) → if- ( 𝜑 , 𝜓 , 𝜒 ) )