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

Theorem ad2antlr 707
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.)
Hypothesis
Ref Expression
ad2ant.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ad2antlr  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )

Proof of Theorem ad2antlr
StepHypRef Expression
1 ad2ant.1 . . 3  |-  ( ph  ->  ps )
21adantr 451 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantll 694 1  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ad3antlr  711  simplr  731  simplrl  736  simplrr  737  ax11eq  2165  ax11el  2166  tfindsg  4688  frsn  4797  sofld  5158  soex  5159  foun  5529  fcof1o  5845  foeqcnvco  5846  f1eqcocnv  5847  caovord3  6075  curry1  6252  curry2  6255  smores2  6413  smo11  6423  smoord  6424  oesuclem  6566  oelim  6575  oaordi  6586  oaass  6601  odi  6619  omass  6620  oen0  6626  oelim2  6635  nnaordi  6658  eceqoveq  6806  resixpfo  6897  boxcutc  6902  xpdom2  7000  domunsncan  7005  omxpenlem  7006  mapen  7068  xpmapenlem  7071  mapdom2  7075  php3  7090  onomeneq  7093  fineqvlem  7120  xpfi  7173  fiint  7178  dffi3  7229  marypha1lem  7231  ordtypelem7  7284  wemaplem3  7308  brwdom2  7332  unxpwdom2  7347  cantnfle  7417  cantnflt  7418  r1pwss  7501  rankval3b  7543  carddomi2  7648  isinffi  7670  fidomtri  7671  acndom  7723  dfac9  7807  dfac12lem1  7814  dfac12lem2  7815  infxp  7886  ackbij1lem16  7906  ackbij2lem3  7912  fictb  7916  cofsmo  7940  cfsmolem  7941  cfcof  7945  infpssrlem4  7977  fin23lem39  8021  isf32lem2  8025  isf32lem3  8026  fin1a2lem12  8082  fin1a2lem13  8083  fin12  8084  axdc3lem4  8124  axdc4lem  8126  ttukeylem3  8183  carden  8218  axrepnd  8261  canthwelem  8317  inawinalem  8356  gchina  8366  r1limwun  8403  inar1  8442  inatsk  8445  tskuni  8450  intgru  8481  nqereu  8598  ltexnq  8644  npex  8655  elnp  8656  prlem936  8716  recexsrlem  8770  mul02lem1  9033  lemul12a  9659  lediv12a  9694  lediv2a  9695  creur  9785  peano5nni  9794  nndiv  9831  rpnnen1lem1  10389  rpnnen1lem2  10390  rpnnen1lem3  10391  rpnnen1lem5  10393  xrmax2  10552  qextltlem  10576  xpncan  10618  xmulneg1  10636  xmulge0  10651  xlemul1a  10655  xrsupsslem  10672  xrinfmsslem  10673  xrub  10677  supxrun  10681  supxrunb1  10685  supxrunb2  10686  supxrbnd  10694  ixxub  10724  ixxlb  10725  elioc2  10760  elico2  10761  elicc2  10762  difreicc  10814  modid  11040  seqf1olem1  11132  facndiv  11348  faclbnd  11350  bcval5  11377  hashdom  11408  hashfacen  11439  seqcoll  11448  revccat  11531  seqshft  11627  sqrmo  11784  absmax  11860  rexico  11884  cau3lem  11885  limsupval2  12001  rlim2lt  12018  o1lo1  12058  rlimconst  12065  climrlim2  12068  2clim  12093  rlimcn2  12111  reccn2  12117  cn1lem  12118  o1of2  12133  lo1const  12141  climsqz  12161  climsqz2  12162  rlimsqzlem  12169  isercolllem2  12186  isercoll  12188  climsup  12190  climcau  12191  caucvgrlem2  12194  iseralt  12204  sumeq2ii  12213  fsum2dlem  12280  fsum0diag2  12292  cvgcmp  12321  cvgcmpce  12323  climcnds  12357  divrcnv  12358  mertenslem1  12387  mertens  12389  efaddlem  12421  tanaddlem  12493  sqr2irr  12574  dvdseq  12623  dvdsext  12626  odd2np1  12634  bitsf1  12684  smuval2  12720  qredeq  12832  qredeu  12833  exprmfct  12836  isprm5  12838  rpexp1i  12847  nonsq  12877  iserodd  12935  pcz  12980  fldivp1  12992  pcfac  12994  expnprm  12997  prmpwdvds  12998  prmreclem5  13014  vdwapf  13066  vdwnnlem2  13090  0ramcl  13117  setscom  13223  firest  13386  isacs2  13604  mreacs  13609  acsfn  13610  acsfn1  13612  ressffth  13861  setcmon  13968  uncfcurf  14062  drsdirfi  14121  lubid  14165  resmhm  14485  resmhm2  14486  mhmco  14488  pwsdiagmhm  14494  gsumwsubmcl  14510  gsumwmhm  14516  gsumwspan  14517  isgrpinv  14581  mulgz  14637  resghm  14748  cntzsubm  14860  cntzmhm  14863  odf1  14924  gexdvds  14944  pgpfi  14965  sylow3lem6  14992  lsmub1x  15006  lsmless12  15021  efgred2  15111  efgcpbllemb  15113  torsubg  15195  prmcyg  15229  ghmcyg  15231  gsumval3  15240  dprdfadd  15304  subgdmdprd  15318  dprdsn  15320  dmdprdsplitlem  15321  dmdprdsplit2lem  15329  ablfacrp  15350  ablfac1b  15354  ablfac2  15373  mgpress  15385  irredrmul  15538  isdrng2  15571  drngmul0or  15582  issubdrg  15619  islss3  15765  lmhmco  15849  lmhmplusg  15850  pwsdiaglmhm  15863  lvecvs0or  15910  lbsextlem2  15961  2idlcpbl  16035  issubassa2  16133  coe1tmmul2  16401  coe1tmmul  16402  qsssubdrg  16487  prmirredlem  16502  mulgrhm2  16517  znidomb  16571  znunit  16573  cyggic  16582  pjfo  16671  obslbs  16686  tgdom  16772  fctop  16797  pptbas  16801  elcls3  16876  toponmre  16886  maxlp  16934  restcld  16959  ssrest  16963  cnfval  17019  cnpfval  17020  iscnp3  17030  subbascn  17040  ssidcn  17041  cnpnei  17049  cncls2  17058  cncls  17059  cnntr  17060  cncnp  17065  restcnrm  17146  cmpsublem  17182  cmpsub  17183  cmpcld  17185  uncmp  17186  hauscmplem  17189  cmpfi  17191  iunconlem  17209  2ndcrest  17236  2ndcctbss  17237  2ndcomap  17240  2ndcsep  17241  1stcelcls  17243  lly1stc  17278  1stckgenlem  17304  ptval  17321  ptbasfi  17332  txcls  17355  tx1cn  17359  ptclsg  17365  xkoccn  17369  upxp  17373  txlly  17386  pthaus  17388  txhaus  17397  xkohaus  17403  xkococnlem  17409  tgqtop  17459  qtopcld  17460  reghmph  17540  ptcmpfi  17560  filcon  17630  fbasrn  17631  filuni  17632  isufil2  17655  ssufl  17665  ufileu  17666  filufint  17667  ufilen  17677  rnelfm  17700  flimopn  17722  flimclsi  17725  hauspwpwf1  17734  isfcls  17756  fcfval  17780  alexsublem  17790  alexsubALTlem2  17794  alexsubALTlem3  17795  alexsubALTlem4  17796  ptcmplem2  17799  ptcmplem3  17800  symgtgp  17836  opnsubg  17842  clsnsg  17844  tsmsres  17878  tsmsf1o  17879  stdbdmet  18114  metcnp  18139  isngp2  18171  subgngp  18203  ngptgp  18204  tngtopn  18218  sranlm  18247  nlmvscn  18250  nmo0  18296  nmoco  18298  qdensere  18331  iocopnst  18491  oprpiece1res2  18503  evth2  18511  xlebnum  18516  lebnumii  18517  pcoass  18575  nmoleub2lem3  18649  nmhmcn  18654  lmnn  18742  cfilfcls  18753  iscmet3lem1  18770  iscmet3lem2  18771  causs  18777  equivcfil  18778  lmclim  18781  lmcau  18791  flimcfil  18792  cmetss  18793  relcmpcmet  18795  bcthlem4  18802  bcthlem5  18803  minveclem3  18846  ovoliunlem2  18915  ovolicc2lem4  18932  nulmbl2  18947  iundisj  18958  ioombl1lem4  18971  vitalilem1  19016  vitali  19021  mbfconstlem  19037  mbfimaicc  19041  mbfimaopnlem  19063  mbfsup  19072  i1fd  19089  i1fmullem  19102  i1fadd  19103  itg1addlem4  19107  itg1addlem5  19108  i1fres  19113  itg10a  19118  itg1climres  19122  mbfi1fseqlem3  19125  mbfi1fseqlem4  19126  mbfi1fseqlem5  19127  itg2const2  19149  itg2seq  19150  itg2monolem1  19158  itg2mono  19161  itg2i1fseqle  19162  itg2cnlem1  19169  iblitg  19176  ibl0  19194  itgss  19219  itgeqa  19221  iblabsr  19237  iblmulc2  19238  bddmulibl  19246  dvnff  19325  dvcobr  19348  dvrec  19357  dvmptfsum  19375  dvexp3  19378  c1liplem1  19396  c1lip1  19397  dvgt0lem1  19402  evlslem3  19451  evlseu  19453  evlsval  19456  tdeglem4  19499  ply1divex  19575  q1pval  19592  fta1g  19606  plyco0  19627  plyeq0lem  19645  plymullem1  19649  plyco  19676  coemullem  19684  coemulhi  19688  coemulc  19689  coe1termlem  19692  dgrlt  19700  dgrco  19709  plycjlem  19710  dvply1  19717  plydivex  19730  fta1  19741  aalioulem2  19766  aalioulem3  19767  aalioulem6  19770  aaliou  19771  taylfval  19791  ulmcaulem  19824  ulmcau  19825  itgulm  19837  pserdvlem2  19857  pilem2  19881  divlogrlim  20035  logcnlem5  20046  advlogexp  20055  cxpcn3  20141  atantayl2  20287  leibpi  20291  birthdaylem3  20301  rlimcnp  20313  cxplim  20319  cxploglim2  20326  ftalem3  20365  basellem2  20372  mumullem1  20470  sqff1o  20473  muinv  20486  chtublem  20503  vmasum  20508  logfac2  20509  mersenne  20519  dchrptlem1  20556  bposlem1  20576  bposlem3  20578  bposlem5  20580  lgslem4  20591  lgsval2lem  20598  lgsmod  20613  lgsdir2lem4  20618  lgsdinn0  20632  lgsquad2lem2  20651  lgsquad3  20653  2sqlem6  20661  2sqlem7  20662  dchrisumlem3  20693  dchrmusumlema  20695  dchrmusum2  20696  dchrvmasumlem1  20697  dchrvmasum2lem  20698  dchrvmasumlem2  20700  dchrvmasumiflem1  20703  dchrisum0lema  20716  dchrisum0lem2a  20719  dchrisum0lem2  20720  mulog2sumlem2  20737  selberg  20750  pntsval2  20778  pntibnd  20795  pntlem3  20811  ostthlem1  20829  ostth2lem2  20836  ostth3  20840  grpoidinv  20928  grpoideu  20929  nvmul0or  21265  vacn  21322  smcnlem  21325  nmoub3i  21406  nmoo0  21424  blocnilem  21437  ubthlem1  21504  ubthlem2  21505  ubthlem3  21506  minvecolem3  21510  hvmul0or  21659  hvmulcan  21706  hvaddsub4  21712  his35  21722  occon  21921  ocorth  21925  occl  21938  chscllem2  22272  5oalem1  22288  5oalem2  22289  3oalem2  22297  pjds3i  22347  nmopub2tALT  22544  nmfnleub2  22561  hmopadj2  22576  0cnop  22614  0cnfn  22615  nmophmi  22666  cnlnadjlem6  22707  leopnmid  22773  nmopleid  22774  opsqrlem1  22775  pjss2coi  22799  pjssdif1i  22810  pj3cor1i  22844  mdsl0  22945  mdslmd1lem1  22960  mdslmd1lem2  22961  csmdsymi  22969  superpos  22989  atomli  23017  chirredlem2  23026  chirredlem3  23027  atcvat3i  23031  atcvat4i  23032  mdsymlem5  23042  cdjreui  23067  cdj1i  23068  disjdifprg  23160  iundisjf  23171  iundisjfi  23301  ishashinf  23311  xaddeq0  23339  xrsmulgzz  23342  xrge0adddir  23353  pnfneige0  23405  lmxrge0  23406  cnextfval  23412  restutopopn  23449  metustid  23496  metustbl  23508  metutop  23509  gsumesum  23627  esumlub  23628  esumcst  23631  insiga  23696  measinb  23749  cntmeas  23754  imambfm  23786  rrvsum  23886  ballotlemsima  23947  derangenlem  23986  subfacp1lem6  24000  conpcon  24050  txscon  24056  iseupa  24165  eupath2  24188  mulge0b  24372  ntrivcvg  24402  prodeq2ii  24416  fundmpss  24507  dftrpred3g  24621  poseq  24638  soseq  24639  sltval2  24695  nobndlem6  24736  brbtwn2  24919  colinearalglem4  24923  colinearalg  24924  axsegconlem8  24938  axsegconlem9  24939  axsegconlem10  24940  ax5seglem3  24945  ax5seglem5  24947  axbtwnid  24953  axlowdimlem17  24972  axeuclid  24977  axcontlem2  24979  axcontlem7  24984  axcontlem8  24985  lxflflp1  25314  itg2addnclem  25317  itg2addnclem2  25318  itg2addnc  25319  itg2gt0cn  25320  iblabsnclem  25328  iblmulc2nc  25330  ftc1cnnc  25339  elicc3  25377  finminlem  25380  nn0prpwlem  25387  lfinpfin  25452  neibastop3  25460  fgmin  25468  filbcmb  25581  sdclem1  25602  fdc  25604  nnubfi  25609  nninfnub  25610  geomcau  25624  istotbnd3  25643  sstotbnd2  25646  sstotbnd3  25648  isbnd3  25656  ssbnd  25660  prdsbnd  25665  cntotbnd  25668  heiborlem8  25690  bfplem2  25695  rrncmslem  25704  rngoisocnv  25760  unichnidl  25804  keridl  25805  prnc  25840  elrfirn  25918  isnacs3  25933  mzpsubmpt  25969  mzprename  25975  lzunuz  25995  eldiophss  26002  eqrabdioph  26005  rexrabdioph  26023  rabdiophlem2  26031  ctbnfien  26049  irrapxlem1  26055  irrapxlem2  26056  irrapxlem4  26058  pell1234qrreccl  26087  pell1234qrmulcl  26088  pell14qrgt0  26092  pell1234qrdich  26094  pell1qrgaplem  26106  pellqrex  26112  reglogltb  26124  reglogleb  26125  monotoddzzfi  26175  oddcomabszz  26177  jm2.24  26198  congsym  26203  acongtr  26213  acongrep  26215  jm2.18  26229  jm2.23  26237  jm2.26a  26241  jm2.26lem3  26242  jm2.27b  26247  rmydioph  26255  setindtr  26265  wepwsolem  26286  dnnumch1  26289  fnwe2lem2  26296  aomclem6  26304  dfac21  26312  islssfg  26316  lnmlsslnm  26327  pwslnm  26344  uvcff  26388  lindfmm  26445  islinds4  26453  lnrfg  26471  dgrsub2  26487  mpaaeu  26503  rngunsnply  26526  f1omvdconj  26537  f1otrspeq  26538  f1omvdco2  26539  symggen  26559  matassa  26629  acsfn1p  26655  cntzsdrg  26658  idomodle  26660  fmuldfeqlem1  26860  fmuldfeq  26861  climrec  26877  climinf  26880  climsuse  26882  itgsinexp  26897  stoweidlem3  26900  stoweidlem7  26904  stoweidlem14  26911  stoweidlem29  26926  stoweidlem34  26931  stoweidlem46  26943  2reu4a  27115  funressnfv  27141  f1oprg  27240  mpt2xopxnop0  27255  elfznelfzo  27275  nbgraf1olem1  27388  nb3graprlem1  27397  constr3trl  27543  constr3pth  27544  constr3cycl  27545  usgravd0nedg  27579  2pthfrgra  27603  frgrancvvdeqlem3  27624  frgrancvvdeqlemC  27631  frgrancvvdeqlem9  27633  bnj1098  28326  bnj1118  28525  bnj1417  28582  cvrval5  29422  3dim0  29464  pmapglbx  29776  pclfinclN  29957  lhplt  30007  lhpexle1  30015  lhpocnle  30023  lhpjat1  30027  lhpjat2  30028  lhpj1  30029  lhpmcvr  30030  lhpmcvr2  30031  lhpm0atN  30036  lhpmat  30037  ltrnid  30142  trlcl  30171  trlle  30191  cdlemc4  30201  cdleme0cp  30221  cdleme0cq  30222  cdlemeulpq  30227  cdleme1b  30233  cdleme1  30234  cdleme2  30235  cdleme3b  30236  cdleme3c  30237  cdlemedb  30304  cdleme27a  30374  docaclN  31132  doca2N  31134  djajN  31145  dihglblem5apreN  31299
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 177  df-an 360
  Copyright terms: Public domain W3C validator