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

Theorem dedth2h 3981
Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 3984 but requires that each hypothesis has exactly one class variable. See also comments in dedth 3980. (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 314 . . 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 3980 . . 3  |-  ( ps 
->  th )
62, 5dedth 3980 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
76imp 427 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1398   ifcif 3929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3930
This theorem is referenced by:  dedth3h  3982  dedth4h  3983  dedth2v  3984  oawordeu  7196  oeoa  7238  unfilem3  7778  eluzadd  11110  eluzsub  11111  sqeqor  12264  binom2  12265  divalglem7  14141  divalg  14145  nmlno0  25908  ipassi  25954  sii  25967  ajfun  25974  ubth  25987  hvnegdi  26182  hvsubeq0  26183  normlem9at  26236  normsub0  26251  norm-ii  26253  norm-iii  26255  normsub  26258  normpyth  26260  norm3adifi  26268  normpar  26270  polid  26274  bcs  26296  shscl  26434  shslej  26496  shincl  26497  pjoc1  26550  pjoml  26552  pjoc2  26555  chincl  26615  chsscon3  26616  chlejb1  26628  chnle  26630  chdmm1  26641  spanun  26661  elspansn2  26683  h1datom  26698  cmbr3  26724  pjoml2  26727  pjoml3  26728  cmcm  26730  cmcm3  26731  lecm  26733  osum  26761  spansnj  26763  pjadji  26801  pjaddi  26802  pjsubi  26804  pjmuli  26805  pjch  26810  pj11  26830  pjnorm  26840  pjpyth  26841  pjnel  26842  hosubcl  26890  hoaddcom  26891  ho0sub  26914  honegsub  26916  eigre  26952  lnopeq0lem2  27123  lnopeq  27126  lnopunii  27129  lnophmi  27135  cvmd  27453  chrelat2  27487  cvexch  27491  mdsym  27529  kur14  28924  abs2sqle  29310  abs2sqlt  29311
  Copyright terms: Public domain W3C validator