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

Theorem ad2antlr 707
Description: Deduction adding 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  2132  ax11el  2133  tfindsg  4651  frsn  4760  sofld  5121  soex  5122  foun  5491  fcof1o  5803  foeqcnvco  5804  f1eqcocnv  5805  caovord3  6033  curry1  6210  curry2  6213  smores2  6371  smo11  6381  smoord  6382  oesuclem  6524  oelim  6533  oaordi  6544  oaass  6559  odi  6577  omass  6578  oen0  6584  oelim2  6593  nnaordi  6616  eceqoveq  6763  resixpfo  6854  boxcutc  6859  xpdom2  6957  domunsncan  6962  omxpenlem  6963  mapen  7025  xpmapenlem  7028  mapdom2  7032  php3  7047  onomeneq  7050  fineqvlem  7077  xpfi  7128  fiint  7133  dffi3  7184  marypha1lem  7186  ordtypelem7  7239  wemaplem3  7263  brwdom2  7287  unxpwdom2  7302  cantnfle  7372  cantnflt  7373  r1pwss  7456  rankval3b  7498  carddomi2  7603  isinffi  7625  fidomtri  7626  acndom  7678  dfac9  7762  dfac12lem1  7769  dfac12lem2  7770  infxp  7841  ackbij1lem16  7861  ackbij2lem3  7867  fictb  7871  cofsmo  7895  cfsmolem  7896  cfcof  7900  infpssrlem4  7932  fin23lem39  7976  isf32lem2  7980  isf32lem3  7981  fin1a2lem12  8037  fin1a2lem13  8038  fin12  8039  axdc3lem4  8079  axdc4lem  8081  ttukeylem3  8138  carden  8173  axrepnd  8216  canthwelem  8272  inawinalem  8311  gchina  8321  r1limwun  8358  inar1  8397  inatsk  8400  tskuni  8405  intgru  8436  nqereu  8553  ltexnq  8599  npex  8610  elnp  8611  prlem936  8671  recexsrlem  8725  mul02lem1  8988  lemul12a  9614  lediv12a  9649  lediv2a  9650  creur  9740  peano5nni  9749  nndiv  9786  rpnnen1lem1  10342  rpnnen1lem2  10343  rpnnen1lem3  10344  rpnnen1lem5  10346  xrmax2  10505  qextltlem  10529  xpncan  10571  xmulneg1  10589  xmulge0  10604  xlemul1a  10608  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  supxrun  10634  supxrunb1  10638  supxrunb2  10639  supxrbnd  10647  ixxub  10677  ixxlb  10678  elioc2  10713  elico2  10714  elicc2  10715  difreicc  10767  modid  10993  seqf1olem1  11085  facndiv  11301  faclbnd  11303  bcval5  11330  hashdom  11361  hashfacen  11392  seqcoll  11401  revccat  11484  seqshft  11580  sqrmo  11737  absmax  11813  rexico  11837  cau3lem  11838  limsupval2  11954  rlim2lt  11971  o1lo1  12011  rlimconst  12018  climrlim2  12021  2clim  12046  rlimcn2  12064  reccn2  12070  cn1lem  12071  o1of2  12086  lo1const  12094  climsqz  12114  climsqz2  12115  rlimsqzlem  12122  isercolllem2  12139  isercoll  12141  climsup  12143  climcau  12144  caucvgrlem2  12147  iseralt  12157  sumeq2ii  12166  fsum2dlem  12233  fsum0diag2  12245  cvgcmp  12274  cvgcmpce  12276  climcnds  12310  divrcnv  12311  mertenslem1  12340  mertens  12342  efaddlem  12374  tanaddlem  12446  sqr2irr  12527  dvdseq  12576  dvdsext  12579  odd2np1  12587  bitsf1  12637  smuval2  12673  qredeq  12785  qredeu  12786  exprmfct  12789  isprm5  12791  rpexp1i  12800  nonsq  12830  iserodd  12888  pcz  12933  fldivp1  12945  pcfac  12947  expnprm  12950  prmpwdvds  12951  prmreclem5  12967  vdwapf  13019  vdwnnlem2  13043  0ramcl  13070  setscom  13176  firest  13337  isacs2  13555  mreacs  13560  acsfn  13561  acsfn1  13563  ressffth  13812  setcmon  13919  uncfcurf  14013  drsdirfi  14072  lubid  14116  resmhm  14436  resmhm2  14437  mhmco  14439  pwsdiagmhm  14445  gsumwsubmcl  14461  gsumwmhm  14467  gsumwspan  14468  isgrpinv  14532  mulgz  14588  resghm  14699  cntzsubm  14811  cntzmhm  14814  odf1  14875  gexdvds  14895  pgpfi  14916  sylow3lem6  14943  lsmub1x  14957  lsmless12  14972  efgred2  15062  efgcpbllemb  15064  torsubg  15146  prmcyg  15180  ghmcyg  15182  gsumval3  15191  dprdfadd  15255  subgdmdprd  15269  dprdsn  15271  dmdprdsplitlem  15272  dmdprdsplit2lem  15280  ablfacrp  15301  ablfac1b  15305  ablfac2  15324  mgpress  15336  irredrmul  15489  isdrng2  15522  drngmul0or  15533  issubdrg  15570  islss3  15716  lmhmco  15800  lmhmplusg  15801  pwsdiaglmhm  15814  lvecvs0or  15861  lbsextlem2  15912  2idlcpbl  15986  issubassa2  16084  coe1tmmul2  16352  coe1tmmul  16353  qsssubdrg  16431  prmirredlem  16446  mulgrhm2  16461  znidomb  16515  znunit  16517  cyggic  16526  pjfo  16615  obslbs  16630  tgdom  16716  fctop  16741  pptbas  16745  elcls3  16820  toponmre  16830  maxlp  16878  restcld  16903  ssrest  16907  cnfval  16963  cnpfval  16964  iscnp3  16974  subbascn  16984  ssidcn  16985  cnpnei  16993  cncls2  17002  cncls  17003  cnntr  17004  cncnp  17009  restcnrm  17090  cmpsublem  17126  cmpsub  17127  cmpcld  17129  uncmp  17130  hauscmplem  17133  cmpfi  17135  iunconlem  17153  2ndcrest  17180  2ndcctbss  17181  2ndcomap  17184  2ndcsep  17185  1stcelcls  17187  lly1stc  17222  1stckgenlem  17248  ptval  17265  ptbasfi  17276  txcls  17299  tx1cn  17303  ptclsg  17309  xkoccn  17313  upxp  17317  txlly  17330  pthaus  17332  txhaus  17341  xkohaus  17347  xkococnlem  17353  tgqtop  17403  qtopcld  17404  reghmph  17484  ptcmpfi  17504  filcon  17578  fbasrn  17579  filuni  17580  isufil2  17603  ssufl  17613  ufileu  17614  filufint  17615  ufilen  17625  rnelfm  17648  flimopn  17670  flimclsi  17673  hauspwpwf1  17682  isfcls  17704  fcfval  17728  alexsublem  17738  alexsubALTlem2  17742  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem2  17747  ptcmplem3  17748  symgtgp  17784  opnsubg  17790  clsnsg  17792  tsmsres  17826  tsmsf1o  17827  stdbdmet  18062  metcnp  18087  isngp2  18119  subgngp  18151  ngptgp  18152  tngtopn  18166  sranlm  18195  nlmvscn  18198  nmo0  18244  nmoco  18246  qdensere  18279  iocopnst  18438  oprpiece1res2  18450  evth2  18458  xlebnum  18463  lebnumii  18464  pcoass  18522  nmoleub2lem3  18596  nmhmcn  18601  lmnn  18689  cfilfcls  18700  iscmet3lem1  18717  iscmet3lem2  18718  causs  18724  equivcfil  18725  lmclim  18728  lmcau  18738  flimcfil  18739  cmetss  18740  relcmpcmet  18742  bcthlem4  18749  bcthlem5  18750  minveclem3  18793  ovoliunlem2  18862  ovolicc2lem4  18879  nulmbl2  18894  iundisj  18905  ioombl1lem4  18918  vitalilem1  18963  vitali  18968  mbfconstlem  18984  mbfimaicc  18988  mbfimaopnlem  19010  mbfsup  19019  i1fd  19036  i1fmullem  19049  i1fadd  19050  itg1addlem4  19054  itg1addlem5  19055  i1fres  19060  itg10a  19065  itg1climres  19069  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  itg2const2  19096  itg2seq  19097  itg2monolem1  19105  itg2mono  19108  itg2i1fseqle  19109  itg2cnlem1  19116  iblitg  19123  ibl0  19141  itgss  19166  itgeqa  19168  iblabsr  19184  iblmulc2  19185  bddmulibl  19193  dvnff  19272  dvcobr  19295  dvrec  19304  dvmptfsum  19322  dvexp3  19325  c1liplem1  19343  c1lip1  19344  dvgt0lem1  19349  evlslem3  19398  evlseu  19400  evlsval  19403  tdeglem4  19446  ply1divex  19522  q1pval  19539  fta1g  19553  plyco0  19574  plyeq0lem  19592  plymullem1  19596  plyco  19623  coemullem  19631  coemulhi  19635  coemulc  19636  coe1termlem  19639  dgrlt  19647  dgrco  19656  plycjlem  19657  dvply1  19664  plydivex  19677  fta1  19688  aalioulem2  19713  aalioulem3  19714  aalioulem6  19717  aaliou  19718  taylfval  19738  ulmcaulem  19771  ulmcau  19772  itgulm  19784  pserdvlem2  19804  pilem2  19828  divlogrlim  19982  logcnlem5  19993  advlogexp  20002  cxpcn3  20088  atantayl2  20234  leibpi  20238  birthdaylem3  20248  rlimcnp  20260  cxplim  20266  cxploglim2  20273  ftalem3  20312  basellem2  20319  mumullem1  20417  sqff1o  20420  muinv  20433  chtublem  20450  vmasum  20455  logfac2  20456  mersenne  20466  dchrptlem1  20503  bposlem1  20523  bposlem3  20525  bposlem5  20527  lgslem4  20538  lgsval2lem  20545  lgsmod  20560  lgsdir2lem4  20565  lgsdinn0  20579  lgsquad2lem2  20598  lgsquad3  20600  2sqlem6  20608  2sqlem7  20609  dchrisumlem3  20640  dchrmusumlema  20642  dchrmusum2  20643  dchrvmasumlem1  20644  dchrvmasum2lem  20645  dchrvmasumlem2  20647  dchrvmasumiflem1  20650  dchrisum0lema  20663  dchrisum0lem2a  20666  dchrisum0lem2  20667  mulog2sumlem2  20684  selberg  20697  pntsval2  20725  pntibnd  20742  pntlem3  20758  ostthlem1  20776  ostth2lem2  20783  ostth3  20787  grpoidinv  20875  grpoideu  20876  nvmul0or  21210  vacn  21267  smcnlem  21270  nmoub3i  21351  nmoo0  21369  blocnilem  21382  ubthlem1  21449  ubthlem2  21450  ubthlem3  21451  minvecolem3  21455  hvmul0or  21604  hvmulcan  21651  hvaddsub4  21657  his35  21667  occon  21866  ocorth  21870  occl  21883  chscllem2  22217  5oalem1  22233  5oalem2  22234  3oalem2  22242  pjds3i  22292  nmopub2tALT  22489  nmfnleub2  22506  hmopadj2  22521  0cnop  22559  0cnfn  22560  nmophmi  22611  cnlnadjlem6  22652  leopnmid  22718  nmopleid  22719  opsqrlem1  22720  pjss2coi  22744  pjssdif1i  22755  pj3cor1i  22789  mdsl0  22890  mdslmd1lem1  22905  mdslmd1lem2  22906  csmdsymi  22914  superpos  22934  atomli  22962  chirredlem2  22971  chirredlem3  22972  atcvat3i  22976  atcvat4i  22977  mdsymlem5  22987  cdjreui  23012  cdj1i  23013  ballotlemsima  23074  xaddeq0  23304  xrsmulgzz  23307  xrge0adddir  23332  disjdifprg  23352  iundisjfi  23363  iundisjf  23365  pnfneige0  23374  lmxrge0  23375  ishashinf  23389  esumcst  23436  insiga  23498  measinb  23548  cntmeas  23553  imambfm  23567  derangenlem  23702  subfacp1lem6  23716  conpcon  23766  txscon  23772  iseupa  23881  eupath2  23904  mulge0b  24086  fundmpss  24122  dftrpred3g  24236  poseq  24253  soseq  24254  sltval2  24310  nobndlem6  24351  brbtwn2  24533  colinearalglem4  24537  colinearalg  24538  axsegconlem8  24552  axsegconlem9  24553  axsegconlem10  24554  ax5seglem3  24559  ax5seglem5  24561  axbtwnid  24567  axlowdimlem17  24586  axeuclid  24591  axcontlem2  24593  axcontlem7  24598  axcontlem8  24599  mapmapmap  25148  prl2  25169  domrancur1c  25202  geme2  25275  muldisc  25481  osneisi  25531  prcnt  25551  cnpflf4  25564  limptlimpr2lem1  25574  altretop  25600  lvsovso  25626  cmpasso  25773  idsubfun  25858  pdiveql  26168  elicc3  26228  finminlem  26231  nn0prpwlem  26238  lfinpfin  26303  neibastop3  26311  fgmin  26319  filbcmb  26432  sdclem1  26453  fdc  26455  nnubfi  26460  nninfnub  26461  geomcau  26475  istotbnd3  26495  sstotbnd2  26498  sstotbnd3  26500  isbnd3  26508  ssbnd  26512  prdsbnd  26517  cntotbnd  26520  heiborlem8  26542  bfplem2  26547  rrncmslem  26556  rngoisocnv  26612  unichnidl  26656  keridl  26657  prnc  26692  elrfirn  26770  isnacs3  26785  mzpsubmpt  26821  mzprename  26827  lzunuz  26847  eldiophss  26854  eqrabdioph  26857  rexrabdioph  26875  rabdiophlem2  26883  ctbnfien  26901  irrapxlem1  26907  irrapxlem2  26908  irrapxlem4  26910  pell1234qrreccl  26939  pell1234qrmulcl  26940  pell14qrgt0  26944  pell1234qrdich  26946  pell1qrgaplem  26958  pellqrex  26964  reglogltb  26976  reglogleb  26977  monotoddzzfi  27027  oddcomabszz  27029  jm2.24  27050  congsym  27055  acongtr  27065  acongrep  27067  jm2.18  27081  jm2.23  27089  jm2.26a  27093  jm2.26lem3  27094  jm2.27b  27099  rmydioph  27107  setindtr  27117  wepwsolem  27138  dnnumch1  27141  fnwe2lem2  27148  aomclem6  27156  dfac21  27164  islssfg  27168  lnmlsslnm  27179  pwslnm  27196  uvcff  27240  lindfmm  27297  islinds4  27305  lnrfg  27323  dgrsub2  27339  mpaaeu  27355  rngunsnply  27378  f1omvdconj  27389  f1otrspeq  27390  f1omvdco2  27391  symggen  27411  matassa  27481  acsfn1p  27507  cntzsdrg  27510  idomodle  27512  fmuldfeqlem1  27712  fmuldfeq  27713  climrec  27729  climinf  27732  climsuse  27734  itgsinexp  27749  stoweidlem3  27752  stoweidlem7  27756  stoweidlem14  27763  stoweidlem29  27778  stoweidlem34  27783  stoweidlem46  27795  2reu4a  27967  funressnfv  27991  f1oprg  28075  mpt2xopxnop0  28081  bnj1098  28815  bnj1118  29014  bnj1417  29071  cvrval5  29604  3dim0  29646  pmapglbx  29958  pclfinclN  30139  lhplt  30189  lhpexle1  30197  lhpocnle  30205  lhpjat1  30209  lhpjat2  30210  lhpj1  30211  lhpmcvr  30212  lhpmcvr2  30213  lhpm0atN  30218  lhpmat  30219  ltrnid  30324  trlcl  30353  trlle  30373  cdlemc4  30383  cdleme0cp  30403  cdleme0cq  30404  cdlemeulpq  30409  cdleme1b  30415  cdleme1  30416  cdleme2  30417  cdleme3b  30418  cdleme3c  30419  cdlemedb  30486  cdleme27a  30556  docaclN  31314  doca2N  31316  djajN  31327  dihglblem5apreN  31481
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