# Metamath Proof Explorer

## Theorem ifpbi1

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

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

### Proof

Step Hyp Ref Expression
1 imbi1 ${⊢}\left({\phi }↔{\psi }\right)\to \left(\left({\phi }\to {\chi }\right)↔\left({\psi }\to {\chi }\right)\right)$
2 notbi ${⊢}\left({\phi }↔{\psi }\right)↔\left(¬{\phi }↔¬{\psi }\right)$
3 2 biimpi ${⊢}\left({\phi }↔{\psi }\right)\to \left(¬{\phi }↔¬{\psi }\right)$
4 3 imbi1d ${⊢}\left({\phi }↔{\psi }\right)\to \left(\left(¬{\phi }\to {\theta }\right)↔\left(¬{\psi }\to {\theta }\right)\right)$
5 1 4 anbi12d ${⊢}\left({\phi }↔{\psi }\right)\to \left(\left(\left({\phi }\to {\chi }\right)\wedge \left(¬{\phi }\to {\theta }\right)\right)↔\left(\left({\psi }\to {\chi }\right)\wedge \left(¬{\psi }\to {\theta }\right)\right)\right)$
6 dfifp2 ${⊢}if-\left({\phi },{\chi },{\theta }\right)↔\left(\left({\phi }\to {\chi }\right)\wedge \left(¬{\phi }\to {\theta }\right)\right)$
7 dfifp2 ${⊢}if-\left({\psi },{\chi },{\theta }\right)↔\left(\left({\psi }\to {\chi }\right)\wedge \left(¬{\psi }\to {\theta }\right)\right)$
8 5 6 7 3bitr4g ${⊢}\left({\phi }↔{\psi }\right)\to \left(if-\left({\phi },{\chi },{\theta }\right)↔if-\left({\psi },{\chi },{\theta }\right)\right)$