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

Metamath Proof Explorer

Theorem elimhyp

Description: Eliminate a hypothesis containing class variable A when it is known for a specific class B . For more information, see comments in dedth . (Contributed by NM, 15-May-1999)

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

Proof

Step Hyp Ref Expression
1 elimhyp.1 ⊢ A = if φ A B → φ ↔ ψ
2 elimhyp.2 ⊢ B = if φ A B → χ ↔ ψ
3 elimhyp.3 ⊢ χ
4 iftrue ⊢ φ → if φ A B = A
5 4 eqcomd ⊢ φ → A = if φ A B
6 5 1 syl ⊢ φ → φ ↔ ψ
7 6 ibi ⊢ φ → ψ
8 iffalse ⊢ ¬ φ → if φ A B = B
9 8 eqcomd ⊢ ¬ φ → B = if φ A B
10 9 2 syl ⊢ ¬ φ → χ ↔ ψ
11 3 10 mpbii ⊢ ¬ φ → ψ
12 7 11 pm2.61i ⊢ ψ