# Metamath Proof Explorer

## Theorem dedth2h

Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v but requires that each hypothesis have exactly one class variable. See also comments in dedth . (Contributed by NM, 15-May-1999)

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

### Proof

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