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

Metamath Proof Explorer

Theorem elimhyp4v

Description: Eliminate a hypothesis containing 4 class variables (for use with the weak deduction theorem dedth ). (Contributed by NM, 16-Apr-2005)

Ref Expression
Hypotheses elimhyp4v.1 
|- ( A = if ( ph , A , D ) -> ( ph <-> ch ) )
elimhyp4v.2 
|- ( B = if ( ph , B , R ) -> ( ch <-> th ) )
elimhyp4v.3 
|- ( C = if ( ph , C , S ) -> ( th <-> ta ) )
elimhyp4v.4 
|- ( F = if ( ph , F , G ) -> ( ta <-> ps ) )
elimhyp4v.5 
|- ( D = if ( ph , A , D ) -> ( et <-> ze ) )
elimhyp4v.6 
|- ( R = if ( ph , B , R ) -> ( ze <-> si ) )
elimhyp4v.7 
|- ( S = if ( ph , C , S ) -> ( si <-> rh ) )
elimhyp4v.8 
|- ( G = if ( ph , F , G ) -> ( rh <-> ps ) )
elimhyp4v.9 
|- et
Assertion elimhyp4v 
|- ps

Proof

Step Hyp Ref Expression
1 elimhyp4v.1 
 |-  ( A = if ( ph , A , D ) -> ( ph <-> ch ) )
2 elimhyp4v.2 
 |-  ( B = if ( ph , B , R ) -> ( ch <-> th ) )
3 elimhyp4v.3 
 |-  ( C = if ( ph , C , S ) -> ( th <-> ta ) )
4 elimhyp4v.4 
 |-  ( F = if ( ph , F , G ) -> ( ta <-> ps ) )
5 elimhyp4v.5 
 |-  ( D = if ( ph , A , D ) -> ( et <-> ze ) )
6 elimhyp4v.6 
 |-  ( R = if ( ph , B , R ) -> ( ze <-> si ) )
7 elimhyp4v.7 
 |-  ( S = if ( ph , C , S ) -> ( si <-> rh ) )
8 elimhyp4v.8 
 |-  ( G = if ( ph , F , G ) -> ( rh <-> ps ) )
9 elimhyp4v.9 
 |-  et
10 iftrue 
 |-  ( ph -> if ( ph , A , D ) = A )
11 10 eqcomd 
 |-  ( ph -> A = if ( ph , A , D ) )
12 11 1 syl 
 |-  ( ph -> ( ph <-> ch ) )
13 iftrue 
 |-  ( ph -> if ( ph , B , R ) = B )
14 13 eqcomd 
 |-  ( ph -> B = if ( ph , B , R ) )
15 14 2 syl 
 |-  ( ph -> ( ch <-> th ) )
16 12 15 bitrd 
 |-  ( ph -> ( ph <-> th ) )
17 iftrue 
 |-  ( ph -> if ( ph , C , S ) = C )
18 17 eqcomd 
 |-  ( ph -> C = if ( ph , C , S ) )
19 18 3 syl 
 |-  ( ph -> ( th <-> ta ) )
20 iftrue 
 |-  ( ph -> if ( ph , F , G ) = F )
21 20 eqcomd 
 |-  ( ph -> F = if ( ph , F , G ) )
22 21 4 syl 
 |-  ( ph -> ( ta <-> ps ) )
23 16 19 22 3bitrd 
 |-  ( ph -> ( ph <-> ps ) )
24 23 ibi 
 |-  ( ph -> ps )
25 iffalse 
 |-  ( -. ph -> if ( ph , A , D ) = D )
26 25 eqcomd 
 |-  ( -. ph -> D = if ( ph , A , D ) )
27 26 5 syl 
 |-  ( -. ph -> ( et <-> ze ) )
28 iffalse 
 |-  ( -. ph -> if ( ph , B , R ) = R )
29 28 eqcomd 
 |-  ( -. ph -> R = if ( ph , B , R ) )
30 29 6 syl 
 |-  ( -. ph -> ( ze <-> si ) )
31 27 30 bitrd 
 |-  ( -. ph -> ( et <-> si ) )
32 iffalse 
 |-  ( -. ph -> if ( ph , C , S ) = S )
33 32 eqcomd 
 |-  ( -. ph -> S = if ( ph , C , S ) )
34 33 7 syl 
 |-  ( -. ph -> ( si <-> rh ) )
35 iffalse 
 |-  ( -. ph -> if ( ph , F , G ) = G )
36 35 eqcomd 
 |-  ( -. ph -> G = if ( ph , F , G ) )
37 36 8 syl 
 |-  ( -. ph -> ( rh <-> ps ) )
38 31 34 37 3bitrd 
 |-  ( -. ph -> ( et <-> ps ) )
39 9 38 mpbii 
 |-  ( -. ph -> ps )
40 24 39 pm2.61i 
 |-  ps