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 φ A B ψ χ
dedth.2 χ
Assertion dedth φ ψ


Step Hyp Ref Expression
1 dedth.1 A = if φ A B ψ χ
2 dedth.2 χ
3 iftrue φ if φ A B = A
4 3 eqcomd φ A = if φ A B
5 4 1 syl φ ψ χ
6 2 5 mpbiri φ ψ