This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ φ → ψ

Proof

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 ⊢ φ → ψ