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

Theorem ad2ant2r 728
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
ad2ant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ad2ant2r  |-  ( ( ( ph  /\  th )  /\  ( ps  /\  ta ) )  ->  ch )

Proof of Theorem ad2ant2r
StepHypRef Expression
1 ad2ant2.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21adantrr 698 . 2  |-  ( (
ph  /\  ( ps  /\ 
ta ) )  ->  ch )
32adantlr 696 1  |-  ( ( ( ph  /\  th )  /\  ( ps  /\  ta ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  foco  5655  fliftfun  6026  omordi  6801  f1imaen2g  7160  isinf  7314  frfi  7344  acndom2  7927  infxp  8087  cff1  8130  isf32lem7  8231  fpwwe2lem12  8508  inawinalem  8556  inar1  8642  grur1  8687  genpnnp  8874  ltexprlem7  8911  prlem936  8916  reclem3pr  8918  1re  9082  addsub4  9336  muladd  9458  lt2add  9505  mullt0  9539  mulnzcnopr  9660  divmuldiv  9706  divmul24  9710  divmuleq  9711  recdiv  9712  divadddiv  9721  conjmul  9723  prodgt0  9847  ltmul12a  9858  lemul12b  9859  lediv12a  9895  lediv2a  9896  qmulcl  10584  irrmul  10591  xrrege0  10754  xmulge0  10855  ge0addcl  11001  ge0mulcl  11002  ge0xaddcl  11003  ge0xmulcl  11004  fzass4  11082  fzrev  11100  fzm1  11119  serge0  11369  expclzlem  11397  expge0  11408  expge1  11409  lt2sq  11447  le2sq  11448  bernneq  11497  sqrmo  12049  limsupval2  12266  o1lo12  12324  climrlim2  12333  2clim  12358  climsup  12455  tanaddlem  12759  divalglem8  12912  opeo  13179  omeo  13180  pcpremul  13209  pcmul  13217  setscom  13489  fpwipodrs  14582  grplactcnv  14879  ghmpreima  15019  ghmeql  15020  conjghm  15028  pgpfi  15231  lmodprop2d  15998  lidlmcl  16280  xrs1mnd  16728  absabv  16748  opnneissb  17170  cncnpi  17334  pnrmopn  17399  cmpsub  17455  connsub  17476  t1conperf  17491  neitx  17631  txcnmpt  17648  txrest  17655  txdis1cn  17659  tx1stc  17674  qtopcn  17738  trfg  17915  rnelfmlem  17976  flffbas  18019  nmo0  18761  nmoid  18768  cfilfcls  19219  iscmet3lem2  19237  caubl  19252  relcmpcmet  19261  ovolun  19387  ovolicc2lem3  19407  volsup  19442  ioombl1lem4  19447  ismbf3d  19538  mbfimaopnlem  19539  i1faddlem  19577  itgle  19693  ellimc2  19756  ftc1a  19913  dgrmul  20180  itgulm  20316  abelthlem8  20347  ptolemy  20396  logdivlt  20508  cxplt3  20583  cxple3  20584  o1cxp  20805  basellem4  20858  sqf11  20914  lgslem3  21074  lgsdir2  21104  lgsne0  21109  lgsquad3  21137  chpo1ubb  21167  vmadivsumb  21169  rpvmasumlem  21173  dchrisum0re  21199  dchrisum0  21206  selberg2b  21238  selberg3lem2  21244  pntrsumbnd  21252  pntrlog2bnd  21270  grporcan  21801  isgrp2d  21815  ablomul  21935  blocni  22298  ubthlem3  22366  htthlem  22412  hvsub4  22531  shscli  22811  elspansn4  23067  5oalem2  23149  hosub4  23308  hmops  23515  hmopco  23518  adjadd  23588  hstpyth  23724  hstles  23726  mdsl0  23805  mdslmd1lem2  23821  chirredlem1  23885  chirredlem2  23886  chirredlem3  23887  chirredlem4  23888  mdsymlem6  23903  cdj3lem2b  23932  esumpcvgval  24460  wfr3g  25529  frr3g  25573  nocvxmin  25638  axcontlem2  25896  mblfinlem3  26236  ismblfin  26237  itg2addnc  26249  ftc1cnnc  26269  reftr  26360  tailfb  26397  filbcmb  26433  prdsbnd  26493  ismtyval  26500  heiborlem8  26518  ghomco  26549  mzpindd  26794  mulltgt0  27660  stoweidlem46  27762  cshwleneq  28231  usgra2adedgspth  28268
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator