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

Theorem elimhyp 3991
Description: Eliminate a hypothesis containing class variable  A when it is known for a specific class  B. For more information, see comments in dedth 3984. (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 3938 . . . . 5  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
21eqcomd 2468 . . . 4  |-  ( ph  ->  A  =  if (
ph ,  A ,  B ) )
3 elimhyp.1 . . . 4  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( ph  <->  ps )
)
42, 3syl 16 . . 3  |-  ( ph  ->  ( ph  <->  ps )
)
54ibi 241 . 2  |-  ( ph  ->  ps )
6 elimhyp.3 . . 3  |-  ch
7 iffalse 3941 . . . . 5  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
87eqcomd 2468 . . . 4  |-  ( -. 
ph  ->  B  =  if ( ph ,  A ,  B ) )
9 elimhyp.2 . . . 4  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( ch  <->  ps )
)
108, 9syl 16 . . 3  |-  ( -. 
ph  ->  ( ch  <->  ps )
)
116, 10mpbii 211 . 2  |-  ( -. 
ph  ->  ps )
125, 11pm2.61i 164 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    = wceq 1374   ifcif 3932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-if 3933
This theorem is referenced by:  elimel  3995  elimf  5721  oeoa  7236  oeoe  7238  limensuc  7684  axcc4dom  8810  elimne0  9575  elimgt0  10367  elimge0  10368  2ndcdisj  19716  siilem2  25429  normlem7tALT  25698  hhsssh  25847  shintcl  25910  chintcl  25912  spanun  26125  elunop2  26594  lnophm  26600  nmbdfnlb  26631  hmopidmch  26734  hmopidmpj  26735  chirred  26976  limsucncmp  29474  elimhyps  33639  elimhyps2  33642
  Copyright terms: Public domain W3C validator