# Metamath Proof Explorer

## Theorem dedth

Description: Weak deduction theorem that eliminates a hypothesis ph , making it become an antecedent. We assume that a proof exists for ph when the class variable A is replaced with a specific class B . The hypothesis ch should be assigned to the inference, and the inference hypothesis eliminated with elimhyp . If the inference has other hypotheses with class variable A , these can be kept by assigning keephyp to them. For more information, see the Weak Deduction Theorem page mmdeduction.html . (Contributed by NM, 15-May-1999)

Ref Expression
Hypotheses dedth.1 ${⊢}{A}=if\left({\phi },{A},{B}\right)\to \left({\psi }↔{\chi }\right)$
dedth.2 ${⊢}{\chi }$
Assertion dedth ${⊢}{\phi }\to {\psi }$

### Proof

Step Hyp Ref Expression
1 dedth.1 ${⊢}{A}=if\left({\phi },{A},{B}\right)\to \left({\psi }↔{\chi }\right)$
2 dedth.2 ${⊢}{\chi }$
3 iftrue ${⊢}{\phi }\to if\left({\phi },{A},{B}\right)={A}$
4 3 eqcomd ${⊢}{\phi }\to {A}=if\left({\phi },{A},{B}\right)$
5 4 1 syl ${⊢}{\phi }\to \left({\psi }↔{\chi }\right)$
6 2 5 mpbiri ${⊢}{\phi }\to {\psi }$