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

Theorem elimhyp 3779
Description: Eliminate a hypothesis containing class variable  A when it is known for a specific class  B. For more information, see comments in dedth 3772. (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 3737 . . . . 5  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
21eqcomd 2440 . . . 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 233 . 2  |-  ( ph  ->  ps )
6 elimhyp.3 . . 3  |-  ch
7 iffalse 3738 . . . . 5  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
87eqcomd 2440 . . . 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 203 . 2  |-  ( -. 
ph  ->  ps )
125, 11pm2.61i 158 1  |-  ps
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    = wceq 1652   ifcif 3731
This theorem is referenced by:  elimel  3783  elimf  5582  oeoa  6832  oeoe  6834  limensuc  7276  axcc4dom  8313  elimne0  9074  elimgt0  9838  elimge0  9839  2ndcdisj  17511  siilem2  22345  normlem7tALT  22613  hhsssh  22761  shintcl  22824  chintcl  22826  spanun  23039  elunop2  23508  lnophm  23514  nmbdfnlb  23545  hmopidmch  23648  hmopidmpj  23649  chirred  23890  limsucncmp  26188
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-if 3732
  Copyright terms: Public domain W3C validator