# Metamath Proof Explorer

## Theorem dedth3h

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

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

### Proof

Step Hyp Ref Expression
1 dedth3h.1 ${⊢}{A}=if\left({\phi },{A},{D}\right)\to \left({\theta }↔{\tau }\right)$
2 dedth3h.2 ${⊢}{B}=if\left({\psi },{B},{R}\right)\to \left({\tau }↔{\eta }\right)$
3 dedth3h.3 ${⊢}{C}=if\left({\chi },{C},{S}\right)\to \left({\eta }↔{\zeta }\right)$
4 dedth3h.4 ${⊢}{\zeta }$
5 1 imbi2d ${⊢}{A}=if\left({\phi },{A},{D}\right)\to \left(\left(\left({\psi }\wedge {\chi }\right)\to {\theta }\right)↔\left(\left({\psi }\wedge {\chi }\right)\to {\tau }\right)\right)$
6 2 3 4 dedth2h ${⊢}\left({\psi }\wedge {\chi }\right)\to {\tau }$
7 5 6 dedth ${⊢}{\phi }\to \left(\left({\psi }\wedge {\chi }\right)\to {\theta }\right)$
8 7 3impib ${⊢}\left({\phi }\wedge {\psi }\wedge {\chi }\right)\to {\theta }$