Metamath Proof Explorer

Theorem 3orbi123

Description: pm4.39 with a 3-conjunct antecedent. This proof is 3orbi123VD automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 3orbi123 ${⊢}\left(\left({\phi }↔{\psi }\right)\wedge \left({\chi }↔{\theta }\right)\wedge \left({\tau }↔{\eta }\right)\right)\to \left(\left({\phi }\vee {\chi }\vee {\tau }\right)↔\left({\psi }\vee {\theta }\vee {\eta }\right)\right)$

Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left(\left({\phi }↔{\psi }\right)\wedge \left({\chi }↔{\theta }\right)\wedge \left({\tau }↔{\eta }\right)\right)\to \left({\phi }↔{\psi }\right)$
2 simp2 ${⊢}\left(\left({\phi }↔{\psi }\right)\wedge \left({\chi }↔{\theta }\right)\wedge \left({\tau }↔{\eta }\right)\right)\to \left({\chi }↔{\theta }\right)$
3 simp3 ${⊢}\left(\left({\phi }↔{\psi }\right)\wedge \left({\chi }↔{\theta }\right)\wedge \left({\tau }↔{\eta }\right)\right)\to \left({\tau }↔{\eta }\right)$
4 1 2 3 3orbi123d ${⊢}\left(\left({\phi }↔{\psi }\right)\wedge \left({\chi }↔{\theta }\right)\wedge \left({\tau }↔{\eta }\right)\right)\to \left(\left({\phi }\vee {\chi }\vee {\tau }\right)↔\left({\psi }\vee {\theta }\vee {\eta }\right)\right)$