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

Theorem dedth2h 3783
Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 3786 but requires that each hypothesis has exactly one class variable. See also comments in dedth 3782. (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 309 . . 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 3782 . . 3  |-  ( ps 
->  th )
62, 5dedth 3782 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
76imp 420 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653   ifcif 3741
This theorem is referenced by:  dedth3h  3784  dedth4h  3785  dedth2v  3786  oawordeu  6800  oeoa  6842  unfilem3  7375  eluzadd  10516  eluzsub  10517  sqeqor  11497  binom2  11498  divalglem7  12921  divalg  12925  nmlno0  22298  ipassi  22344  sii  22357  ajfun  22364  ubth  22377  hvnegdi  22571  hvsubeq0  22572  normlem9at  22625  normsub0  22640  norm-ii  22642  norm-iii  22644  normsub  22647  normpyth  22649  norm3adifi  22657  normpar  22659  polid  22663  bcs  22685  shscl  22822  shslej  22884  shincl  22885  pjoc1  22938  pjoml  22940  pjoc2  22943  chincl  23003  chsscon3  23004  chlejb1  23016  chnle  23018  chdmm1  23029  spanun  23049  elspansn2  23071  h1datom  23086  cmbr3  23112  pjoml2  23115  pjoml3  23116  cmcm  23118  cmcm3  23119  lecm  23121  osum  23149  spansnj  23151  pjadji  23189  pjaddi  23190  pjsubi  23192  pjmuli  23193  pjch  23198  pj11  23218  pjnorm  23228  pjpyth  23229  pjnel  23230  hosubcl  23278  hoaddcom  23279  ho0sub  23302  honegsub  23304  eigre  23340  lnopeq0lem2  23511  lnopeq  23514  lnopunii  23517  lnophmi  23523  cvmd  23841  chrelat2  23875  cvexch  23879  mdsym  23917  kur14  24904  abs2sqle  25122  abs2sqlt  25123
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-if 3742
  Copyright terms: Public domain W3C validator