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

Metamath Proof Explorer

Theorem keephyp

Description: Transform a hypothesis ps that we want to keep (but contains the same class variable A used in the eliminated hypothesis) for use with the weak deduction theorem. (Contributed by NM, 15-May-1999)

Ref Expression
Hypotheses keephyp.1 ⊢ A = if φ A B → ψ ↔ θ
keephyp.2 ⊢ B = if φ A B → χ ↔ θ
keephyp.3 ⊢ ψ
keephyp.4 ⊢ χ
Assertion keephyp ⊢ θ

Proof

Step Hyp Ref Expression
1 keephyp.1 ⊢ A = if φ A B → ψ ↔ θ
2 keephyp.2 ⊢ B = if φ A B → χ ↔ θ
3 keephyp.3 ⊢ ψ
4 keephyp.4 ⊢ χ
5 1 2 ifboth ⊢ ψ ∧ χ → θ
6 3 4 5 mp2an ⊢ θ