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

Metamath Proof Explorer

Theorem keephyp2v

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

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

Proof

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