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

Theorem dedth2h 3607
Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 3610 but requires that each hypothesis has exactly one class variable. See also comments in dedth 3606. (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 3606 . . 3  |-  ( ps 
->  th )
62, 5dedth 3606 . 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 1623   ifcif 3565
This theorem is referenced by:  dedth3h  3608  dedth4h  3609  dedth2v  3610  oawordeu  6553  oeoa  6595  unfilem3  7123  eluzadd  10256  eluzsub  10257  sqeqor  11217  binom2  11218  divalglem7  12598  divalg  12602  nmlno0  21373  ipassi  21419  sii  21432  ajfun  21439  ubth  21452  hvnegdi  21646  hvsubeq0  21647  normlem9at  21700  normsub0  21715  norm-ii  21717  norm-iii  21719  normsub  21722  normpyth  21724  norm3adifi  21732  normpar  21734  polid  21738  bcs  21760  shscl  21897  shslej  21959  shincl  21960  pjoc1  22013  pjoml  22015  pjoc2  22018  chincl  22078  chsscon3  22079  chlejb1  22091  chnle  22093  chdmm1  22104  spanun  22124  elspansn2  22146  h1datom  22161  cmbr3  22187  pjoml2  22190  pjoml3  22191  cmcm  22193  cmcm3  22194  lecm  22196  osum  22224  spansnj  22226  pjadji  22264  pjaddi  22265  pjsubi  22267  pjmuli  22268  pjch  22273  pj11  22293  pjnorm  22303  pjpyth  22304  pjnel  22305  hosubcl  22353  hoaddcom  22354  ho0sub  22377  honegsub  22379  eigre  22415  lnopeq0lem2  22586  lnopeq  22589  lnopunii  22592  lnophmi  22598  cvmd  22916  chrelat2  22950  cvexch  22954  mdsym  22992  kur14  23747  abs2sqle  24016  abs2sqlt  24017  ab2rexexg  25122  selsubf3g  25992
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566
  Copyright terms: Public domain W3C validator