Metamath Proof Explorer

Theorem dedth4h

Description: Weak deduction theorem eliminating four hypotheses. See comments in dedth2h . (Contributed by NM, 16-May-1999)

Ref Expression
Hypotheses dedth4h.1 ${⊢}{A}=if\left({\phi },{A},{R}\right)\to \left({\tau }↔{\eta }\right)$
dedth4h.2 ${⊢}{B}=if\left({\psi },{B},{S}\right)\to \left({\eta }↔{\zeta }\right)$
dedth4h.3 ${⊢}{C}=if\left({\chi },{C},{F}\right)\to \left({\zeta }↔{\sigma }\right)$
dedth4h.4 ${⊢}{D}=if\left({\theta },{D},{G}\right)\to \left({\sigma }↔{\rho }\right)$
dedth4h.5 ${⊢}{\rho }$
Assertion dedth4h ${⊢}\left(\left({\phi }\wedge {\psi }\right)\wedge \left({\chi }\wedge {\theta }\right)\right)\to {\tau }$

Proof

Step Hyp Ref Expression
1 dedth4h.1 ${⊢}{A}=if\left({\phi },{A},{R}\right)\to \left({\tau }↔{\eta }\right)$
2 dedth4h.2 ${⊢}{B}=if\left({\psi },{B},{S}\right)\to \left({\eta }↔{\zeta }\right)$
3 dedth4h.3 ${⊢}{C}=if\left({\chi },{C},{F}\right)\to \left({\zeta }↔{\sigma }\right)$
4 dedth4h.4 ${⊢}{D}=if\left({\theta },{D},{G}\right)\to \left({\sigma }↔{\rho }\right)$
5 dedth4h.5 ${⊢}{\rho }$
6 1 imbi2d ${⊢}{A}=if\left({\phi },{A},{R}\right)\to \left(\left(\left({\chi }\wedge {\theta }\right)\to {\tau }\right)↔\left(\left({\chi }\wedge {\theta }\right)\to {\eta }\right)\right)$
7 2 imbi2d ${⊢}{B}=if\left({\psi },{B},{S}\right)\to \left(\left(\left({\chi }\wedge {\theta }\right)\to {\eta }\right)↔\left(\left({\chi }\wedge {\theta }\right)\to {\zeta }\right)\right)$
8 3 4 5 dedth2h ${⊢}\left({\chi }\wedge {\theta }\right)\to {\zeta }$
9 6 7 8 dedth2h ${⊢}\left({\phi }\wedge {\psi }\right)\to \left(\left({\chi }\wedge {\theta }\right)\to {\tau }\right)$
10 9 imp ${⊢}\left(\left({\phi }\wedge {\psi }\right)\wedge \left({\chi }\wedge {\theta }\right)\right)\to {\tau }$