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

Metamath Proof Explorer

Theorem elimdhyp

Description: Version of elimhyp where the hypothesis is deduced from the final antecedent. See divalg for an example of its use. (Contributed by Paul Chapman, 25-Mar-2008)

Ref Expression
Hypotheses elimdhyp.1 
|- ( ph -> ps )
elimdhyp.2 
|- ( A = if ( ph , A , B ) -> ( ps <-> ch ) )
elimdhyp.3 
|- ( B = if ( ph , A , B ) -> ( th <-> ch ) )
elimdhyp.4 
|- th
Assertion elimdhyp 
|- ch

Proof

Step Hyp Ref Expression
1 elimdhyp.1 
 |-  ( ph -> ps )
2 elimdhyp.2 
 |-  ( A = if ( ph , A , B ) -> ( ps <-> ch ) )
3 elimdhyp.3 
 |-  ( B = if ( ph , A , B ) -> ( th <-> ch ) )
4 elimdhyp.4 
 |-  th
5 iftrue 
 |-  ( ph -> if ( ph , A , B ) = A )
6 5 eqcomd 
 |-  ( ph -> A = if ( ph , A , B ) )
7 6 2 syl 
 |-  ( ph -> ( ps <-> ch ) )
8 1 7 mpbid 
 |-  ( ph -> ch )
9 iffalse 
 |-  ( -. ph -> if ( ph , A , B ) = B )
10 9 eqcomd 
 |-  ( -. ph -> B = if ( ph , A , B ) )
11 10 3 syl 
 |-  ( -. ph -> ( th <-> ch ) )
12 4 11 mpbii 
 |-  ( -. ph -> ch )
13 8 12 pm2.61i 
 |-  ch