Theorem ifbid

Description: Equivalence deduction for conditional operators. (Contributed by NM, 18-Apr-2005)

	Ref	Expression
Hypothesis	ifbid.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
Assertion	ifbid	$$⊢\phi \to if\left(\psi ,A,B\right)=if\left(\chi ,A,B\right)$$

Proof

Step	Hyp	Ref	Expression
1		ifbid.1	$$⊢\phi \to \left(\psi \leftrightarrow \chi \right)$$
2		ifbi	$$⊢\left(\psi \leftrightarrow \chi \right)\to if\left(\psi ,A,B\right)=if\left(\chi ,A,B\right)$$
3	1 2	syl	$$⊢\phi \to if\left(\psi ,A,B\right)=if\left(\chi ,A,B\right)$$