# Metamath Proof Explorer

## Theorem ifbi

Description: Equivalence theorem for conditional operators. (Contributed by Raph Levien, 15-Jan-2004)

Ref Expression
Assertion ifbi ${⊢}\left({\phi }↔{\psi }\right)\to if\left({\phi },{A},{B}\right)=if\left({\psi },{A},{B}\right)$

### Proof

Step Hyp Ref Expression
1 dfbi3 ${⊢}\left({\phi }↔{\psi }\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left(¬{\phi }\wedge ¬{\psi }\right)\right)$
2 iftrue ${⊢}{\phi }\to if\left({\phi },{A},{B}\right)={A}$
3 iftrue ${⊢}{\psi }\to if\left({\psi },{A},{B}\right)={A}$
4 3 eqcomd ${⊢}{\psi }\to {A}=if\left({\psi },{A},{B}\right)$
5 2 4 sylan9eq ${⊢}\left({\phi }\wedge {\psi }\right)\to if\left({\phi },{A},{B}\right)=if\left({\psi },{A},{B}\right)$
6 iffalse ${⊢}¬{\phi }\to if\left({\phi },{A},{B}\right)={B}$
7 iffalse ${⊢}¬{\psi }\to if\left({\psi },{A},{B}\right)={B}$
8 7 eqcomd ${⊢}¬{\psi }\to {B}=if\left({\psi },{A},{B}\right)$
9 6 8 sylan9eq ${⊢}\left(¬{\phi }\wedge ¬{\psi }\right)\to if\left({\phi },{A},{B}\right)=if\left({\psi },{A},{B}\right)$
10 5 9 jaoi ${⊢}\left(\left({\phi }\wedge {\psi }\right)\vee \left(¬{\phi }\wedge ¬{\psi }\right)\right)\to if\left({\phi },{A},{B}\right)=if\left({\psi },{A},{B}\right)$
11 1 10 sylbi ${⊢}\left({\phi }↔{\psi }\right)\to if\left({\phi },{A},{B}\right)=if\left({\psi },{A},{B}\right)$