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

Theorem dedth2h 3620
Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 3623 but requires that each hypothesis has exactly one class variable. See also comments in dedth 3619. (Contributed by NM, 15-May-1999.)
Hypotheses
Ref Expression
dedth2h.1  |-  ( A  =  if ( ph ,  A ,  C )  ->  ( ch  <->  th )
)
dedth2h.2  |-  ( B  =  if ( ps ,  B ,  D
)  ->  ( th  <->  ta ) )
dedth2h.3  |-  ta
Assertion
Ref Expression
dedth2h  |-  ( (
ph  /\  ps )  ->  ch )

Proof of Theorem dedth2h
StepHypRef Expression
1 dedth2h.1 . . . 4  |-  ( A  =  if ( ph ,  A ,  C )  ->  ( ch  <->  th )
)
21imbi2d 307 . . 3  |-  ( A  =  if ( ph ,  A ,  C )  ->  ( ( ps 
->  ch )  <->  ( ps  ->  th ) ) )
3 dedth2h.2 . . . 4  |-  ( B  =  if ( ps ,  B ,  D
)  ->  ( th  <->  ta ) )
4 dedth2h.3 . . . 4  |-  ta
53, 4dedth 3619 . . 3  |-  ( ps 
->  th )
62, 5dedth 3619 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
76imp 418 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632   ifcif 3578
This theorem is referenced by:  dedth3h  3621  dedth4h  3622  dedth2v  3623  oawordeu  6569  oeoa  6611  unfilem3  7139  eluzadd  10272  eluzsub  10273  sqeqor  11233  binom2  11234  divalglem7  12614  divalg  12618  nmlno0  21389  ipassi  21435  sii  21448  ajfun  21455  ubth  21468  hvnegdi  21662  hvsubeq0  21663  normlem9at  21716  normsub0  21731  norm-ii  21733  norm-iii  21735  normsub  21738  normpyth  21740  norm3adifi  21748  normpar  21750  polid  21754  bcs  21776  shscl  21913  shslej  21975  shincl  21976  pjoc1  22029  pjoml  22031  pjoc2  22034  chincl  22094  chsscon3  22095  chlejb1  22107  chnle  22109  chdmm1  22120  spanun  22140  elspansn2  22162  h1datom  22177  cmbr3  22203  pjoml2  22206  pjoml3  22207  cmcm  22209  cmcm3  22210  lecm  22212  osum  22240  spansnj  22242  pjadji  22280  pjaddi  22281  pjsubi  22283  pjmuli  22284  pjch  22289  pj11  22309  pjnorm  22319  pjpyth  22320  pjnel  22321  hosubcl  22369  hoaddcom  22370  ho0sub  22393  honegsub  22395  eigre  22431  lnopeq0lem2  22602  lnopeq  22605  lnopunii  22608  lnophmi  22614  cvmd  22932  chrelat2  22966  cvexch  22970  mdsym  23008  kur14  23762  abs2sqle  24031  abs2sqlt  24032  ab2rexexg  25225  selsubf3g  26095
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