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

Theorem elimhyp 3613
Description: Eliminate a hypothesis containing class variable  A when it is known for a specific class  B. For more information, see comments in dedth 3606. (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 3571 . . . . 5  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
21eqcomd 2288 . . . 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 3572 . . . . 5  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
87eqcomd 2288 . . . 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 1623   ifcif 3565
This theorem is referenced by:  elimel  3617  elimf  5388  oeoa  6595  oeoe  6597  limensuc  7038  axcc4dom  8067  elimne0  8829  elimgt0  9592  elimge0  9593  2ndcdisj  17182  siilem2  21430  normlem7tALT  21698  hhsssh  21846  shintcl  21909  chintcl  21911  spanun  22124  elunop2  22593  lnophm  22599  nmbdfnlb  22630  hmopidmch  22733  hmopidmpj  22734  chirred  22975  limsucncmp  24885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566
  Copyright terms: Public domain W3C validator