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

Theorem dedth2h 3943
Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v 3946 but requires that each hypothesis has exactly one class variable. See also comments in dedth 3942. (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 316 . . 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 3942 . . 3  |-  ( ps 
->  th )
62, 5dedth 3942 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
76imp 429 1  |-  ( (
ph  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370   ifcif 3892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-if 3893
This theorem is referenced by:  dedth3h  3944  dedth4h  3945  dedth2v  3946  oawordeu  7097  oeoa  7139  unfilem3  7682  eluzadd  10993  eluzsub  10994  sqeqor  12090  binom2  12091  divalglem7  13714  divalg  13718  nmlno0  24340  ipassi  24386  sii  24399  ajfun  24406  ubth  24419  hvnegdi  24614  hvsubeq0  24615  normlem9at  24668  normsub0  24683  norm-ii  24685  norm-iii  24687  normsub  24690  normpyth  24692  norm3adifi  24700  normpar  24702  polid  24706  bcs  24728  shscl  24866  shslej  24928  shincl  24929  pjoc1  24982  pjoml  24984  pjoc2  24987  chincl  25047  chsscon3  25048  chlejb1  25060  chnle  25062  chdmm1  25073  spanun  25093  elspansn2  25115  h1datom  25130  cmbr3  25156  pjoml2  25159  pjoml3  25160  cmcm  25162  cmcm3  25163  lecm  25165  osum  25193  spansnj  25195  pjadji  25233  pjaddi  25234  pjsubi  25236  pjmuli  25237  pjch  25242  pj11  25262  pjnorm  25272  pjpyth  25273  pjnel  25274  hosubcl  25322  hoaddcom  25323  ho0sub  25346  honegsub  25348  eigre  25384  lnopeq0lem2  25555  lnopeq  25558  lnopunii  25561  lnophmi  25567  cvmd  25885  chrelat2  25919  cvexch  25923  mdsym  25961  kur14  27241  abs2sqle  27462  abs2sqlt  27463
  Copyright terms: Public domain W3C validator