Theorem axfrege58a

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

	Ref	Expression
Assertion	axfrege58a	$$⊢\left(\psi \wedge \chi \right)\to if-\left(\phi ,\psi ,\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		anifp	$$⊢\left(\psi \wedge \chi \right)\to if-\left(\phi ,\psi ,\chi \right)$$