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

Theorem ad2antlr 709
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 453 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantll 696 1  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  ad3antlr  713  simplr  733  simplrl  738  simplrr  739  ax11eq  2272  ax11el  2273  tfindsg  4843  frsn  4951  sofld  5321  soex  5322  foun  5696  f1oprg  5721  fcof1o  6029  foeqcnvco  6030  f1eqcocnv  6031  caovord3  6263  curry1  6441  curry2  6444  f1o2ndf1  6457  mpt2xopxnop0  6469  smores2  6619  smo11  6629  smoord  6630  oesuclem  6772  oelim  6781  oaordi  6792  oaass  6807  odi  6825  omass  6826  oen0  6832  oelim2  6841  nnaordi  6864  eceqoveq  7012  resixpfo  7103  boxcutc  7108  xpdom2  7206  domunsncan  7211  omxpenlem  7212  mapen  7274  xpmapenlem  7277  mapdom2  7281  php3  7296  onomeneq  7299  fineqvlem  7326  xpfi  7381  fiint  7386  dffi3  7439  marypha1lem  7441  ordtypelem7  7496  wemaplem3  7520  brwdom2  7544  unxpwdom2  7559  cantnfle  7629  cantnflt  7630  r1pwss  7713  rankval3b  7755  carddomi2  7862  isinffi  7884  fidomtri  7885  acndom  7937  dfac9  8021  dfac12lem1  8028  dfac12lem2  8029  ackbij1lem16  8120  ackbij2lem3  8126  fictb  8130  cofsmo  8154  cfsmolem  8155  cfcof  8159  infpssrlem4  8191  fin23lem39  8235  isf32lem2  8239  isf32lem3  8240  fin1a2lem12  8296  fin1a2lem13  8297  fin12  8298  axdc3lem4  8338  axdc4lem  8340  ttukeylem3  8396  carden  8431  axrepnd  8474  canthwelem  8530  inawinalem  8569  gchina  8579  r1limwun  8616  inar1  8655  inatsk  8658  tskuni  8663  intgru  8694  nqereu  8811  ltexnq  8857  npex  8868  elnp  8869  prlem936  8929  recexsrlem  8983  mul02lem1  9247  lemul12a  9873  lediv12a  9908  lediv2a  9909  creur  9999  peano5nni  10008  nndiv  10045  rpnnen1lem1  10605  rpnnen1lem2  10606  rpnnen1lem3  10607  rpnnen1lem5  10609  xrmax2  10769  qextltlem  10793  xpncan  10835  xmulneg1  10853  xmulge0  10868  xlemul1a  10872  xrsupsslem  10890  xrinfmsslem  10891  xrub  10895  supxrun  10899  supxrunb1  10903  supxrunb2  10904  supxrbnd  10912  ixxub  10942  ixxlb  10943  elioc2  10978  elico2  10979  elicc2  10980  difreicc  11033  elfznelfzo  11197  modid  11275  seqf1olem1  11367  facndiv  11584  faclbnd  11586  bcval5  11614  hashdom  11658  hashfacen  11708  seqcoll  11717  brfi1indlem  11719  brfi1uzind  11720  revccat  11803  seqshft  11905  sqrmo  12062  absmax  12138  rexico  12162  cau3lem  12163  limsupval2  12279  rlim2lt  12296  o1lo1  12336  rlimconst  12343  climrlim2  12346  2clim  12371  rlimcn2  12389  reccn2  12395  cn1lem  12396  o1of2  12411  lo1const  12419  climsqz  12439  climsqz2  12440  isercolllem2  12464  isercoll  12466  climsup  12468  climcau  12469  caucvgrlem2  12473  iseralt  12483  sumeq2ii  12492  fsum2dlem  12559  fsum0diag2  12571  cvgcmp  12600  cvgcmpce  12602  climcnds  12636  divrcnv  12637  mertenslem1  12666  mertens  12668  efaddlem  12700  tanaddlem  12772  sqr2irr  12853  dvdseq  12902  dvdsext  12905  odd2np1  12913  bitsf1  12963  smuval2  12999  qredeq  13111  qredeu  13112  exprmfct  13115  isprm5  13117  rpexp1i  13126  nonsq  13156  iserodd  13214  pcz  13259  fldivp1  13271  pcfac  13273  expnprm  13276  prmpwdvds  13277  prmreclem5  13293  vdwapf  13345  vdwnnlem2  13369  0ramcl  13396  setscom  13502  firest  13665  isacs2  13883  mreacs  13888  acsfn  13889  acsfn1  13891  ressffth  14140  setcmon  14247  uncfcurf  14341  drsdirfi  14400  lubid  14444  resmhm  14764  resmhm2  14765  mhmco  14767  pwsdiagmhm  14773  gsumwsubmcl  14789  gsumwmhm  14795  gsumwspan  14796  isgrpinv  14860  mulgz  14916  resghm  15027  cntzsubm  15139  cntzmhm  15142  odf1  15203  gexdvds  15223  pgpfi  15244  sylow3lem6  15271  lsmub1x  15285  lsmless12  15300  efgred2  15390  efgcpbllemb  15392  torsubg  15474  prmcyg  15508  ghmcyg  15510  gsumval3  15519  dprdfadd  15583  subgdmdprd  15597  dprdsn  15599  dmdprdsplitlem  15600  dmdprdsplit2lem  15608  ablfacrp  15629  ablfac1b  15633  ablfac2  15652  mgpress  15664  irredrmul  15817  isdrng2  15850  drngmul0or  15861  issubdrg  15898  islss3  16040  lmhmco  16124  lmhmplusg  16125  pwsdiaglmhm  16138  lvecvs0or  16185  lbsextlem2  16236  2idlcpbl  16310  issubassa2  16408  coe1tmmul2  16673  coe1tmmul  16674  qsssubdrg  16763  prmirredlem  16778  mulgrhm2  16793  znidomb  16847  znunit  16849  cyggic  16858  pjfo  16947  obslbs  16962  tgdom  17048  fctop  17073  pptbas  17077  elcls3  17152  toponmre  17162  neiptopuni  17199  neiptoptop  17200  neiptopreu  17202  maxlp  17216  ssrest  17245  cnfval  17302  cnpfval  17303  iscnp3  17313  subbascn  17323  ssidcn  17324  cnpnei  17333  cncls2  17342  cncls  17343  cnntr  17344  cncnp  17349  restcnrm  17431  cmpsublem  17467  cmpsub  17468  cmpcld  17470  uncmp  17471  hauscmplem  17474  cmpfi  17476  iunconlem  17495  2ndcrest  17522  2ndcctbss  17523  2ndcomap  17526  2ndcsep  17527  1stcelcls  17529  lly1stc  17564  1stckgenlem  17590  ptval  17607  ptbasfi  17618  txcls  17641  tx1cn  17646  ptclsg  17652  xkoccn  17656  upxp  17660  xkococnlem  17696  imasnopn  17727  imasncld  17728  imasncls  17729  tgqtop  17749  qtopcld  17750  reghmph  17830  ptcmpfi  17850  filcon  17920  fbasrn  17921  filuni  17922  isufil2  17945  ssufl  17955  ufileu  17956  filufint  17957  ufilen  17967  rnelfm  17990  flimopn  18012  flimclsi  18015  hauspwpwf1  18024  isfcls  18046  fcfval  18070  alexsublem  18080  alexsubALTlem2  18084  alexsubALTlem3  18085  alexsubALTlem4  18086  ptcmplem2  18089  ptcmplem3  18090  cnextfval  18098  symgtgp  18136  opnsubg  18142  clsnsg  18144  tsmsres  18178  tsmsf1o  18179  restutopopn  18273  neipcfilu  18331  stdbdmet  18551  metcnp  18576  metustidOLD  18594  metustid  18595  metustsymOLD  18596  metustblOLD  18615  metustbl  18616  metutopOLD  18617  psmetutop  18618  isngp2  18649  subgngp  18681  ngptgp  18682  tngtopn  18696  sranlm  18725  nlmvscn  18728  nmo0  18774  nmoco  18776  qdensere  18809  iocopnst  18970  oprpiece1res2  18982  evth2  18990  xlebnum  18995  lebnumii  18996  pcoass  19054  nmoleub2lem3  19128  nmhmcn  19133  lmnn  19221  cfilfcls  19232  iscmet3lem1  19249  iscmet3lem2  19250  causs  19256  equivcfil  19257  lmclim  19260  lmcau  19270  flimcfil  19271  cmetss  19272  relcmpcmet  19274  bcthlem4  19285  bcthlem5  19286  minveclem3  19335  ovoliunlem2  19404  ovolicc2lem4  19421  nulmbl2  19436  iundisj  19447  ioombl1lem4  19460  vitalilem1  19505  vitali  19510  mbfconstlem  19524  mbfimaicc  19528  mbfimaopnlem  19550  mbfsup  19559  i1fd  19576  i1fmullem  19589  i1fadd  19590  itg1addlem4  19594  itg1addlem5  19595  i1fres  19600  itg10a  19605  itg1climres  19609  mbfi1fseqlem3  19612  mbfi1fseqlem4  19613  mbfi1fseqlem5  19614  itg2const2  19636  itg2seq  19637  itg2monolem1  19645  itg2mono  19648  itg2i1fseqle  19649  itg2cnlem1  19656  iblitg  19663  ibl0  19681  itgss  19706  itgeqa  19708  iblabsr  19724  iblmulc2  19725  bddmulibl  19733  dvnff  19814  dvcobr  19837  dvrec  19846  dvmptfsum  19864  dvexp3  19867  c1liplem1  19885  c1lip1  19886  dvgt0lem1  19891  evlslem3  19940  evlseu  19942  evlsval  19945  tdeglem4  19988  ply1divex  20064  q1pval  20081  fta1g  20095  plyco0  20116  plyeq0lem  20134  plymullem1  20138  plyco  20165  coemullem  20173  coemulhi  20177  coemulc  20178  coe1termlem  20181  dgrlt  20189  dgrco  20198  plycjlem  20199  dvply1  20206  plydivex  20219  fta1  20230  aalioulem2  20255  aalioulem3  20256  aalioulem6  20259  aaliou  20260  taylfval  20280  ulmcaulem  20315  ulmcau  20316  itgulm  20329  pserdvlem2  20349  pilem2  20373  divlogrlim  20531  logcnlem5  20542  advlogexp  20551  cxpcn3  20637  atantayl2  20783  leibpi  20787  birthdaylem3  20797  rlimcnp  20809  cxplim  20815  cxploglim2  20822  ftalem3  20862  basellem2  20869  mumullem1  20967  sqff1o  20970  muinv  20983  chtublem  21000  vmasum  21005  logfac2  21006  mersenne  21016  dchrptlem1  21053  bposlem1  21073  bposlem3  21075  bposlem5  21077  lgslem4  21088  lgsval2lem  21095  lgsmod  21110  lgsdir2lem4  21115  lgsdinn0  21129  lgsquad2lem2  21148  lgsquad3  21150  2sqlem6  21158  2sqlem7  21159  dchrisumlem3  21190  dchrmusumlema  21192  dchrmusum2  21193  dchrvmasumlem1  21194  dchrvmasum2lem  21195  dchrvmasumlem2  21197  dchrvmasumiflem1  21200  dchrisum0lema  21213  dchrisum0lem2a  21216  dchrisum0lem2  21217  mulog2sumlem2  21234  selberg  21247  pntsval2  21275  pntibnd  21292  pntlem3  21308  ostthlem1  21326  ostth2lem2  21333  ostth3  21337  usgrares1  21429  nbgraf1olem1  21456  nb3graprlem1  21465  cusgrasize2inds  21491  cusgrafilem2  21494  2wlklem1  21602  constr2wlk  21603  constr3trl  21651  constr3pth  21652  constr3cycl  21653  usgravd0nedg  21688  iseupa  21692  eupath2  21707  grpoidinv  21801  grpoideu  21802  nvmul0or  22138  vacn  22195  smcnlem  22198  nmoub3i  22279  nmoo0  22297  blocnilem  22310  ubthlem1  22377  ubthlem2  22378  ubthlem3  22379  minvecolem3  22383  hvmul0or  22532  hvmulcan  22579  hvaddsub4  22585  his35  22595  occon  22794  ocorth  22798  occl  22811  chscllem2  23145  5oalem1  23161  5oalem2  23162  3oalem2  23170  pjds3i  23220  nmopub2tALT  23417  nmfnleub2  23434  hmopadj2  23449  0cnop  23487  0cnfn  23488  nmophmi  23539  cnlnadjlem6  23580  leopnmid  23646  nmopleid  23647  opsqrlem1  23648  pjss2coi  23672  pjssdif1i  23683  pj3cor1i  23717  mdsl0  23818  mdslmd1lem1  23833  mdslmd1lem2  23834  csmdsymi  23842  superpos  23862  atomli  23890  chirredlem2  23899  chirredlem3  23900  atcvat3i  23904  atcvat4i  23905  mdsymlem5  23915  cdjreui  23940  cdj1i  23941  disjdifprg  24022  iundisjf  24034  xaddeq0  24124  iundisjfi  24157  ishashinf  24164  xrsmulgzz  24205  xrge0adddir  24220  ofldchr  24249  subofld  24250  xrge0iifiso  24326  pnfneige0  24341  lmxrge0  24342  gsumesum  24456  esumlub  24457  esumcst  24460  insiga  24525  measinb  24580  cntmeas  24585  imambfm  24617  rrvsum  24717  ballotlemsv  24772  ballotlemsima  24778  derangenlem  24862  subfacp1lem6  24876  conpcon  24927  txscon  24933  mulge0b  25196  ntrivcvg  25230  prodeq2ii  25244  fprod2dlem  25309  fundmpss  25395  dftrpred3g  25516  poseq  25533  soseq  25534  sltval2  25616  nobndlem6  25657  brbtwn2  25849  colinearalglem4  25853  colinearalg  25854  axsegconlem8  25868  axsegconlem9  25869  axsegconlem10  25870  ax5seglem3  25875  ax5seglem5  25877  axbtwnid  25883  axlowdimlem17  25902  axeuclid  25907  axcontlem2  25909  axcontlem7  25914  axcontlem8  25915  lxflflp1  26249  mblfinlem2  26256  mblfinlem3  26257  ismblfin  26259  cnambfre  26267  itg2addnclem  26270  itg2addnclem2  26271  itg2addnclem3  26272  itg2addnc  26273  itg2gt0cn  26274  iblabsnclem  26282  iblmulc2nc  26284  ftc1cnnc  26293  ftc1anclem5  26298  ftc1anclem6  26299  ftc1anclem7  26300  ftc1anclem8  26301  ftc1anc  26302  finminlem  26335  nn0prpwlem  26339  lfinpfin  26397  neibastop3  26405  fgmin  26413  filbcmb  26456  sdclem1  26461  fdc  26463  nnubfi  26468  nninfnub  26469  geomcau  26479  istotbnd3  26494  sstotbnd3  26499  isbnd3  26507  ssbnd  26511  prdsbnd  26516  cntotbnd  26519  heiborlem8  26541  bfplem2  26546  rrncmslem  26555  rngoisocnv  26611  unichnidl  26655  keridl  26656  prnc  26691  elrfirn  26763  isnacs3  26778  mzpsubmpt  26814  mzprename  26820  lzunuz  26840  eldiophss  26847  eqrabdioph  26850  rexrabdioph  26868  rabdiophlem2  26876  ctbnfien  26893  irrapxlem1  26899  irrapxlem2  26900  irrapxlem4  26902  pell1234qrreccl  26931  pell1234qrmulcl  26932  pell14qrgt0  26936  pell1234qrdich  26938  pell1qrgaplem  26950  pellqrex  26956  reglogltb  26968  reglogleb  26969  monotoddzzfi  27019  oddcomabszz  27021  jm2.24  27042  congsym  27047  acongtr  27057  acongrep  27059  jm2.18  27073  jm2.23  27081  jm2.26a  27085  jm2.26lem3  27086  jm2.27b  27091  rmydioph  27099  setindtr  27109  wepwsolem  27130  dnnumch1  27133  fnwe2lem2  27140  aomclem6  27148  dfac21  27155  islssfg  27159  lnmlsslnm  27170  pwslnm  27187  uvcff  27231  lindfmm  27288  islinds4  27296  lnrfg  27314  dgrsub2  27330  mpaaeu  27346  rngunsnply  27369  f1omvdconj  27380  f1otrspeq  27381  f1omvdco2  27382  symggen  27402  matassa  27472  acsfn1p  27498  cntzsdrg  27501  idomodle  27503  fmuldfeqlem1  27702  fmuldfeq  27703  climrec  27719  climinf  27722  climsuse  27724  itgsinexp  27739  stoweidlem3  27742  stoweidlem7  27746  stoweidlem14  27753  stoweidlem29  27768  stoweidlem34  27773  stoweidlem46  27785  2reu4a  27957  funressnfv  27982  swdeq  28230  swrdccat3  28249  2cshw1lem2  28283  2cshwmod  28291  cshwssizelem1a  28313  cshwssizelem3  28316  cshwsexa  28325  usgra2pthlem1  28348  el2spthonot0  28403  cusgraisrusgra  28449  2pthfrgra  28475  frgrancvvdeqlem3  28495  frgrancvvdeqlemC  28502  frgrancvvdeqlem9  28504  frg2woteu  28518  frg2woteq  28523  bnj1098  29228  bnj1118  29427  bnj1417  29484  cvrval5  30286  3dim0  30328  pmapglbx  30640  pclfinclN  30821  lhplt  30871  lhpexle1  30879  lhpocnle  30887  lhpjat1  30891  lhpjat2  30892  lhpj1  30893  lhpmcvr  30894  lhpmcvr2  30895  lhpm0atN  30900  lhpmat  30901  ltrnid  31006  trlcl  31035  trlle  31055  cdlemc4  31065  cdleme0cp  31085  cdleme0cq  31086  cdlemeulpq  31091  cdleme1b  31097  cdleme1  31098  cdleme2  31099  cdleme3b  31100  cdleme3c  31101  cdlemedb  31168  cdleme27a  31238  docaclN  31996  doca2N  31998  djajN  32009  dihglblem5apreN  32163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator