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

Metamath Proof Explorer

Theorem elimhyp2v

Description: Eliminate a hypothesis containing 2 class variables. (Contributed by NM, 14-Aug-1999)

Ref Expression
Hypotheses elimhyp2v.1 
|- ( A = if ( ph , A , C ) -> ( ph <-> ch ) )
elimhyp2v.2 
|- ( B = if ( ph , B , D ) -> ( ch <-> th ) )
elimhyp2v.3 
|- ( C = if ( ph , A , C ) -> ( ta <-> et ) )
elimhyp2v.4 
|- ( D = if ( ph , B , D ) -> ( et <-> th ) )
elimhyp2v.5 
|- ta
Assertion elimhyp2v 
|- th

Proof

Step Hyp Ref Expression
1 elimhyp2v.1 
 |-  ( A = if ( ph , A , C ) -> ( ph <-> ch ) )
2 elimhyp2v.2 
 |-  ( B = if ( ph , B , D ) -> ( ch <-> th ) )
3 elimhyp2v.3 
 |-  ( C = if ( ph , A , C ) -> ( ta <-> et ) )
4 elimhyp2v.4 
 |-  ( D = if ( ph , B , D ) -> ( et <-> th ) )
5 elimhyp2v.5 
 |-  ta
6 iftrue 
 |-  ( ph -> if ( ph , A , C ) = A )
7 6 eqcomd 
 |-  ( ph -> A = if ( ph , A , C ) )
8 7 1 syl 
 |-  ( ph -> ( ph <-> ch ) )
9 iftrue 
 |-  ( ph -> if ( ph , B , D ) = B )
10 9 eqcomd 
 |-  ( ph -> B = if ( ph , B , D ) )
11 10 2 syl 
 |-  ( ph -> ( ch <-> th ) )
12 8 11 bitrd 
 |-  ( ph -> ( ph <-> th ) )
13 12 ibi 
 |-  ( ph -> th )
14 iffalse 
 |-  ( -. ph -> if ( ph , A , C ) = C )
15 14 eqcomd 
 |-  ( -. ph -> C = if ( ph , A , C ) )
16 15 3 syl 
 |-  ( -. ph -> ( ta <-> et ) )
17 iffalse 
 |-  ( -. ph -> if ( ph , B , D ) = D )
18 17 eqcomd 
 |-  ( -. ph -> D = if ( ph , B , D ) )
19 18 4 syl 
 |-  ( -. ph -> ( et <-> th ) )
20 16 19 bitrd 
 |-  ( -. ph -> ( ta <-> th ) )
21 5 20 mpbii 
 |-  ( -. ph -> th )
22 13 21 pm2.61i 
 |-  th