Theorem axfrege52a

Description: Justification for ax-frege52a . (Contributed by RP, 17-Apr-2020)

	Ref	Expression
Assertion	axfrege52a	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( if- ( 𝜑 , 𝜃 , 𝜒 ) → if- ( 𝜓 , 𝜃 , 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ifpbi1	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( if- ( 𝜑 , 𝜃 , 𝜒 ) ↔ if- ( 𝜓 , 𝜃 , 𝜒 ) ) )
2	1	biimpd	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( if- ( 𝜑 , 𝜃 , 𝜒 ) → if- ( 𝜓 , 𝜃 , 𝜒 ) ) )