# Metamath Proof Explorer

## Theorem ifpbi2

Description: Equivalence theorem for conditional logical operators. (Contributed by RP, 14-Apr-2020)

Ref Expression
Assertion ifpbi2 ${⊢}\left({\phi }↔{\psi }\right)\to \left(if-\left({\chi },{\phi },{\theta }\right)↔if-\left({\chi },{\psi },{\theta }\right)\right)$

### Proof

Step Hyp Ref Expression
1 imbi2 ${⊢}\left({\phi }↔{\psi }\right)\to \left(\left({\chi }\to {\phi }\right)↔\left({\chi }\to {\psi }\right)\right)$
2 1 anbi1d ${⊢}\left({\phi }↔{\psi }\right)\to \left(\left(\left({\chi }\to {\phi }\right)\wedge \left(¬{\chi }\to {\theta }\right)\right)↔\left(\left({\chi }\to {\psi }\right)\wedge \left(¬{\chi }\to {\theta }\right)\right)\right)$
3 dfifp2 ${⊢}if-\left({\chi },{\phi },{\theta }\right)↔\left(\left({\chi }\to {\phi }\right)\wedge \left(¬{\chi }\to {\theta }\right)\right)$
4 dfifp2 ${⊢}if-\left({\chi },{\psi },{\theta }\right)↔\left(\left({\chi }\to {\psi }\right)\wedge \left(¬{\chi }\to {\theta }\right)\right)$
5 2 3 4 3bitr4g ${⊢}\left({\phi }↔{\psi }\right)\to \left(if-\left({\chi },{\phi },{\theta }\right)↔if-\left({\chi },{\psi },{\theta }\right)\right)$