MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elimhyp Unicode version

Theorem elimhyp 3626
Description: Eliminate a hypothesis containing class variable  A when it is known for a specific class  B. For more information, see comments in dedth 3619. (Contributed by NM, 15-May-1999.)
Hypotheses
Ref Expression
elimhyp.1  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ph  <->  ps )
)
elimhyp.2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( ch  <->  ps )
)
elimhyp.3  |-  ch
Assertion
Ref Expression
elimhyp  |-  ps

Proof of Theorem elimhyp
StepHypRef Expression
1 iftrue 3584 . . . . 5  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
21eqcomd 2301 . . . 4  |-  ( ph  ->  A  =  if (
ph ,  A ,  B ) )
3 elimhyp.1 . . . 4  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ph  <->  ps )
)
42, 3syl 15 . . 3  |-  ( ph  ->  ( ph  <->  ps )
)
54ibi 232 . 2  |-  ( ph  ->  ps )
6 elimhyp.3 . . 3  |-  ch
7 iffalse 3585 . . . . 5  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
87eqcomd 2301 . . . 4  |-  ( -. 
ph  ->  B  =  if ( ph ,  A ,  B ) )
9 elimhyp.2 . . . 4  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( ch  <->  ps )
)
108, 9syl 15 . . 3  |-  ( -. 
ph  ->  ( ch  <->  ps )
)
116, 10mpbii 202 . 2  |-  ( -. 
ph  ->  ps )
125, 11pm2.61i 156 1  |-  ps
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    = wceq 1632   ifcif 3578
This theorem is referenced by:  elimel  3630  elimf  5404  oeoa  6611  oeoe  6613  limensuc  7054  axcc4dom  8083  elimne0  8845  elimgt0  9608  elimge0  9609  2ndcdisj  17198  siilem2  21446  normlem7tALT  21714  hhsssh  21862  shintcl  21925  chintcl  21927  spanun  22140  elunop2  22609  lnophm  22615  nmbdfnlb  22646  hmopidmch  22749  hmopidmpj  22750  chirred  22991  limsucncmp  24957
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-if 3579
  Copyright terms: Public domain W3C validator