# 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\left({\phi },{A},{B}\right)\to \left({\phi }↔{\psi }\right)$
elimhyp.2 ${⊢}{B}=if\left({\phi },{A},{B}\right)\to \left({\chi }↔{\psi }\right)$
elimhyp.3 ${⊢}{\chi }$
Assertion elimhyp ${⊢}{\psi }$

### Proof

Step Hyp Ref Expression
1 elimhyp.1 ${⊢}{A}=if\left({\phi },{A},{B}\right)\to \left({\phi }↔{\psi }\right)$
2 elimhyp.2 ${⊢}{B}=if\left({\phi },{A},{B}\right)\to \left({\chi }↔{\psi }\right)$
3 elimhyp.3 ${⊢}{\chi }$
4 iftrue ${⊢}{\phi }\to if\left({\phi },{A},{B}\right)={A}$
5 4 eqcomd ${⊢}{\phi }\to {A}=if\left({\phi },{A},{B}\right)$
6 5 1 syl ${⊢}{\phi }\to \left({\phi }↔{\psi }\right)$
7 6 ibi ${⊢}{\phi }\to {\psi }$
8 iffalse ${⊢}¬{\phi }\to if\left({\phi },{A},{B}\right)={B}$
9 8 eqcomd ${⊢}¬{\phi }\to {B}=if\left({\phi },{A},{B}\right)$
10 9 2 syl ${⊢}¬{\phi }\to \left({\chi }↔{\psi }\right)$
11 3 10 mpbii ${⊢}¬{\phi }\to {\psi }$
12 7 11 pm2.61i ${⊢}{\psi }$