# Metamath Proof Explorer

## Theorem ifpbi123dOLD

Description: Obsolete version of ifpbi123d as of 17-Apr-2024. (Contributed by AV, 30-Dec-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses ifpbi123d.1 ${⊢}{\phi }\to \left({\psi }↔{\tau }\right)$
ifpbi123d.2 ${⊢}{\phi }\to \left({\chi }↔{\eta }\right)$
ifpbi123d.3 ${⊢}{\phi }\to \left({\theta }↔{\zeta }\right)$
Assertion ifpbi123dOLD ${⊢}{\phi }\to \left(if-\left({\psi },{\chi },{\theta }\right)↔if-\left({\tau },{\eta },{\zeta }\right)\right)$

### Proof

Step Hyp Ref Expression
1 ifpbi123d.1 ${⊢}{\phi }\to \left({\psi }↔{\tau }\right)$
2 ifpbi123d.2 ${⊢}{\phi }\to \left({\chi }↔{\eta }\right)$
3 ifpbi123d.3 ${⊢}{\phi }\to \left({\theta }↔{\zeta }\right)$
4 1 2 anbi12d ${⊢}{\phi }\to \left(\left({\psi }\wedge {\chi }\right)↔\left({\tau }\wedge {\eta }\right)\right)$
5 1 notbid ${⊢}{\phi }\to \left(¬{\psi }↔¬{\tau }\right)$
6 5 3 anbi12d ${⊢}{\phi }\to \left(\left(¬{\psi }\wedge {\theta }\right)↔\left(¬{\tau }\wedge {\zeta }\right)\right)$
7 4 6 orbi12d ${⊢}{\phi }\to \left(\left(\left({\psi }\wedge {\chi }\right)\vee \left(¬{\psi }\wedge {\theta }\right)\right)↔\left(\left({\tau }\wedge {\eta }\right)\vee \left(¬{\tau }\wedge {\zeta }\right)\right)\right)$
8 df-ifp ${⊢}if-\left({\psi },{\chi },{\theta }\right)↔\left(\left({\psi }\wedge {\chi }\right)\vee \left(¬{\psi }\wedge {\theta }\right)\right)$
9 df-ifp ${⊢}if-\left({\tau },{\eta },{\zeta }\right)↔\left(\left({\tau }\wedge {\eta }\right)\vee \left(¬{\tau }\wedge {\zeta }\right)\right)$
10 7 8 9 3bitr4g ${⊢}{\phi }\to \left(if-\left({\psi },{\chi },{\theta }\right)↔if-\left({\tau },{\eta },{\zeta }\right)\right)$