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

Theorem ad2antlr 708
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 452 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantll 695 1  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  ad3antlr  712  simplr  732  simplrl  737  simplrr  738  ax11eq  2220  ax11el  2221  tfindsg  4773  frsn  4881  sofld  5251  soex  5252  foun  5626  f1oprg  5651  fcof1o  5958  foeqcnvco  5959  f1eqcocnv  5960  caovord3  6192  curry1  6370  curry2  6373  mpt2xopxnop0  6395  smores2  6545  smo11  6555  smoord  6556  oesuclem  6698  oelim  6707  oaordi  6718  oaass  6733  odi  6751  omass  6752  oen0  6758  oelim2  6767  nnaordi  6790  eceqoveq  6938  resixpfo  7029  boxcutc  7034  xpdom2  7132  domunsncan  7137  omxpenlem  7138  mapen  7200  xpmapenlem  7203  mapdom2  7207  php3  7222  onomeneq  7225  fineqvlem  7252  xpfi  7307  fiint  7312  dffi3  7364  marypha1lem  7366  ordtypelem7  7419  wemaplem3  7443  brwdom2  7467  unxpwdom2  7482  cantnfle  7552  cantnflt  7553  r1pwss  7636  rankval3b  7678  carddomi2  7783  isinffi  7805  fidomtri  7806  acndom  7858  dfac9  7942  dfac12lem1  7949  dfac12lem2  7950  ackbij1lem16  8041  ackbij2lem3  8047  fictb  8051  cofsmo  8075  cfsmolem  8076  cfcof  8080  infpssrlem4  8112  fin23lem39  8156  isf32lem2  8160  isf32lem3  8161  fin1a2lem12  8217  fin1a2lem13  8218  fin12  8219  axdc3lem4  8259  axdc4lem  8261  ttukeylem3  8317  carden  8352  axrepnd  8395  canthwelem  8451  inawinalem  8490  gchina  8500  r1limwun  8537  inar1  8576  inatsk  8579  tskuni  8584  intgru  8615  nqereu  8732  ltexnq  8778  npex  8789  elnp  8790  prlem936  8850  recexsrlem  8904  mul02lem1  9167  lemul12a  9793  lediv12a  9828  lediv2a  9829  creur  9919  peano5nni  9928  nndiv  9965  rpnnen1lem1  10525  rpnnen1lem2  10526  rpnnen1lem3  10527  rpnnen1lem5  10529  xrmax2  10689  qextltlem  10713  xpncan  10755  xmulneg1  10773  xmulge0  10788  xlemul1a  10792  xrsupsslem  10810  xrinfmsslem  10811  xrub  10815  supxrun  10819  supxrunb1  10823  supxrunb2  10824  supxrbnd  10832  ixxub  10862  ixxlb  10863  elioc2  10898  elico2  10899  elicc2  10900  difreicc  10953  elfznelfzo  11112  modid  11190  seqf1olem1  11282  facndiv  11499  faclbnd  11501  bcval5  11529  hashdom  11573  hashfacen  11623  seqcoll  11632  brfi1indlem  11634  brfi1uzind  11635  revccat  11718  seqshft  11820  sqrmo  11977  absmax  12053  rexico  12077  cau3lem  12078  limsupval2  12194  rlim2lt  12211  o1lo1  12251  rlimconst  12258  climrlim2  12261  2clim  12286  rlimcn2  12304  reccn2  12310  cn1lem  12311  o1of2  12326  lo1const  12334  climsqz  12354  climsqz2  12355  isercolllem2  12379  isercoll  12381  climsup  12383  climcau  12384  caucvgrlem2  12388  iseralt  12398  sumeq2ii  12407  fsum2dlem  12474  fsum0diag2  12486  cvgcmp  12515  cvgcmpce  12517  climcnds  12551  divrcnv  12552  mertenslem1  12581  mertens  12583  efaddlem  12615  tanaddlem  12687  sqr2irr  12768  dvdseq  12817  dvdsext  12820  odd2np1  12828  bitsf1  12878  smuval2  12914  qredeq  13026  qredeu  13027  exprmfct  13030  isprm5  13032  rpexp1i  13041  nonsq  13071  iserodd  13129  pcz  13174  fldivp1  13186  pcfac  13188  expnprm  13191  prmpwdvds  13192  prmreclem5  13208  vdwapf  13260  vdwnnlem2  13284  0ramcl  13311  setscom  13417  firest  13580  isacs2  13798  mreacs  13803  acsfn  13804  acsfn1  13806  ressffth  14055  setcmon  14162  uncfcurf  14256  drsdirfi  14315  lubid  14359  resmhm  14679  resmhm2  14680  mhmco  14682  pwsdiagmhm  14688  gsumwsubmcl  14704  gsumwmhm  14710  gsumwspan  14711  isgrpinv  14775  mulgz  14831  resghm  14942  cntzsubm  15054  cntzmhm  15057  odf1  15118  gexdvds  15138  pgpfi  15159  sylow3lem6  15186  lsmub1x  15200  lsmless12  15215  efgred2  15305  efgcpbllemb  15307  torsubg  15389  prmcyg  15423  ghmcyg  15425  gsumval3  15434  dprdfadd  15498  subgdmdprd  15512  dprdsn  15514  dmdprdsplitlem  15515  dmdprdsplit2lem  15523  ablfacrp  15544  ablfac1b  15548  ablfac2  15567  mgpress  15579  irredrmul  15732  isdrng2  15765  drngmul0or  15776  issubdrg  15813  islss3  15955  lmhmco  16039  lmhmplusg  16040  pwsdiaglmhm  16053  lvecvs0or  16100  lbsextlem2  16151  2idlcpbl  16225  issubassa2  16323  coe1tmmul2  16588  coe1tmmul  16589  qsssubdrg  16674  prmirredlem  16689  mulgrhm2  16704  znidomb  16758  znunit  16760  cyggic  16769  pjfo  16858  obslbs  16873  tgdom  16959  fctop  16984  pptbas  16988  elcls3  17063  toponmre  17073  neiptopuni  17110  neiptoptop  17111  neiptopreu  17113  maxlp  17126  ssrest  17155  cnfval  17212  cnpfval  17213  iscnp3  17223  subbascn  17233  ssidcn  17234  cnpnei  17243  cncls2  17252  cncls  17253  cnntr  17254  cncnp  17259  restcnrm  17341  cmpsublem  17377  cmpsub  17378  cmpcld  17380  uncmp  17381  hauscmplem  17384  cmpfi  17386  iunconlem  17404  2ndcrest  17431  2ndcctbss  17432  2ndcomap  17435  2ndcsep  17436  1stcelcls  17438  lly1stc  17473  1stckgenlem  17499  ptval  17516  ptbasfi  17527  txcls  17550  tx1cn  17555  ptclsg  17561  xkoccn  17565  upxp  17569  xkococnlem  17605  imasnopn  17636  imasncld  17637  imasncls  17638  tgqtop  17658  qtopcld  17659  reghmph  17739  ptcmpfi  17759  filcon  17829  fbasrn  17830  filuni  17831  isufil2  17854  ssufl  17864  ufileu  17865  filufint  17866  ufilen  17876  rnelfm  17899  flimopn  17921  flimclsi  17924  hauspwpwf1  17933  isfcls  17955  fcfval  17979  alexsublem  17989  alexsubALTlem2  17993  alexsubALTlem3  17994  alexsubALTlem4  17995  ptcmplem2  17998  ptcmplem3  17999  cnextfval  18007  symgtgp  18045  opnsubg  18051  clsnsg  18053  tsmsres  18087  tsmsf1o  18088  restutopopn  18182  neipcfilu  18240  stdbdmet  18429  metcnp  18454  metustid  18467  metustsym  18468  metustbl  18479  metutop  18480  isngp2  18508  subgngp  18540  ngptgp  18541  tngtopn  18555  sranlm  18584  nlmvscn  18587  nmo0  18633  nmoco  18635  qdensere  18668  iocopnst  18829  oprpiece1res2  18841  evth2  18849  xlebnum  18854  lebnumii  18855  pcoass  18913  nmoleub2lem3  18987  nmhmcn  18992  lmnn  19080  cfilfcls  19091  iscmet3lem1  19108  iscmet3lem2  19109  causs  19115  equivcfil  19116  lmclim  19119  lmcau  19129  flimcfil  19130  cmetss  19131  relcmpcmet  19133  bcthlem4  19142  bcthlem5  19143  minveclem3  19190  ovoliunlem2  19259  ovolicc2lem4  19276  nulmbl2  19291  iundisj  19302  ioombl1lem4  19315  vitalilem1  19360  vitali  19365  mbfconstlem  19381  mbfimaicc  19385  mbfimaopnlem  19407  mbfsup  19416  i1fd  19433  i1fmullem  19446  i1fadd  19447  itg1addlem4  19451  itg1addlem5  19452  i1fres  19457  itg10a  19462  itg1climres  19466  mbfi1fseqlem3  19469  mbfi1fseqlem4  19470  mbfi1fseqlem5  19471  itg2const2  19493  itg2seq  19494  itg2monolem1  19502  itg2mono  19505  itg2i1fseqle  19506  itg2cnlem1  19513  iblitg  19520  ibl0  19538  itgss  19563  itgeqa  19565  iblabsr  19581  iblmulc2  19582  bddmulibl  19590  dvnff  19669  dvcobr  19692  dvrec  19701  dvmptfsum  19719  dvexp3  19722  c1liplem1  19740  c1lip1  19741  dvgt0lem1  19746  evlslem3  19795  evlseu  19797  evlsval  19800  tdeglem4  19843  ply1divex  19919  q1pval  19936  fta1g  19950  plyco0  19971  plyeq0lem  19989  plymullem1  19993  plyco  20020  coemullem  20028  coemulhi  20032  coemulc  20033  coe1termlem  20036  dgrlt  20044  dgrco  20053  plycjlem  20054  dvply1  20061  plydivex  20074  fta1  20085  aalioulem2  20110  aalioulem3  20111  aalioulem6  20114  aaliou  20115  taylfval  20135  ulmcaulem  20170  ulmcau  20171  itgulm  20184  pserdvlem2  20204  pilem2  20228  divlogrlim  20386  logcnlem5  20397  advlogexp  20406  cxpcn3  20492  atantayl2  20638  leibpi  20642  birthdaylem3  20652  rlimcnp  20664  cxplim  20670  cxploglim2  20677  ftalem3  20717  basellem2  20724  mumullem1  20822  sqff1o  20825  muinv  20838  chtublem  20855  vmasum  20860  logfac2  20861  mersenne  20871  dchrptlem1  20908  bposlem1  20928  bposlem3  20930  bposlem5  20932  lgslem4  20943  lgsval2lem  20950  lgsmod  20965  lgsdir2lem4  20970  lgsdinn0  20984  lgsquad2lem2  21003  lgsquad3  21005  2sqlem6  21013  2sqlem7  21014  dchrisumlem3  21045  dchrmusumlema  21047  dchrmusum2  21048  dchrvmasumlem1  21049  dchrvmasum2lem  21050  dchrvmasumlem2  21052  dchrvmasumiflem1  21055  dchrisum0lema  21068  dchrisum0lem2a  21071  dchrisum0lem2  21072  mulog2sumlem2  21089  selberg  21102  pntsval2  21130  pntibnd  21147  pntlem3  21163  ostthlem1  21181  ostth2lem2  21188  ostth3  21192  usgrares1  21283  nbgraf1olem1  21310  nb3graprlem1  21319  cusgrasize2inds  21345  cusgrafilem2  21348  constr3trl  21487  constr3pth  21488  constr3cycl  21489  usgravd0nedg  21524  iseupa  21528  eupath2  21543  grpoidinv  21637  grpoideu  21638  nvmul0or  21974  vacn  22031  smcnlem  22034  nmoub3i  22115  nmoo0  22133  blocnilem  22146  ubthlem1  22213  ubthlem2  22214  ubthlem3  22215  minvecolem3  22219  hvmul0or  22368  hvmulcan  22415  hvaddsub4  22421  his35  22431  occon  22630  ocorth  22634  occl  22647  chscllem2  22981  5oalem1  22997  5oalem2  22998  3oalem2  23006  pjds3i  23056  nmopub2tALT  23253  nmfnleub2  23270  hmopadj2  23285  0cnop  23323  0cnfn  23324  nmophmi  23375  cnlnadjlem6  23416  leopnmid  23482  nmopleid  23483  opsqrlem1  23484  pjss2coi  23508  pjssdif1i  23519  pj3cor1i  23553  mdsl0  23654  mdslmd1lem1  23669  mdslmd1lem2  23670  csmdsymi  23678  superpos  23698  atomli  23726  chirredlem2  23735  chirredlem3  23736  atcvat3i  23740  atcvat4i  23741  mdsymlem5  23751  cdjreui  23776  cdj1i  23777  disjdifprg  23854  iundisjf  23865  iundisjfi  23983  ishashinf  23990  xaddeq0  24023  xrsmulgzz  24026  xrge0adddir  24037  ofldchr  24063  subofld  24064  xrge0iifiso  24118  pnfneige0  24133  lmxrge0  24134  gsumesum  24240  esumlub  24241  esumcst  24244  insiga  24309  measinb  24362  cntmeas  24367  imambfm  24399  rrvsum  24484  ballotlemsv  24539  ballotlemsima  24545  derangenlem  24629  subfacp1lem6  24643  conpcon  24694  txscon  24700  mulge0b  24963  ntrivcvg  24997  prodeq2ii  25011  fundmpss  25139  dftrpred3g  25253  poseq  25270  soseq  25271  sltval2  25327  nobndlem6  25368  brbtwn2  25551  colinearalglem4  25555  colinearalg  25556  axsegconlem8  25570  axsegconlem9  25571  axsegconlem10  25572  ax5seglem3  25577  ax5seglem5  25579  axbtwnid  25585  axlowdimlem17  25604  axeuclid  25609  axcontlem2  25611  axcontlem7  25616  axcontlem8  25617  lxflflp1  25945  itg2addnclem  25950  itg2addnclem2  25951  itg2addnc  25952  itg2gt0cn  25953  iblabsnclem  25961  iblmulc2nc  25963  ftc1cnnc  25972  finminlem  26005  nn0prpwlem  26009  lfinpfin  26067  neibastop3  26075  fgmin  26083  filbcmb  26126  sdclem1  26131  fdc  26133  nnubfi  26138  nninfnub  26139  geomcau  26149  istotbnd3  26164  sstotbnd3  26169  isbnd3  26177  ssbnd  26181  prdsbnd  26186  cntotbnd  26189  heiborlem8  26211  bfplem2  26216  rrncmslem  26225  rngoisocnv  26281  unichnidl  26325  keridl  26326  prnc  26361  elrfirn  26433  isnacs3  26448  mzpsubmpt  26484  mzprename  26490  lzunuz  26510  eldiophss  26517  eqrabdioph  26520  rexrabdioph  26538  rabdiophlem2  26546  ctbnfien  26563  irrapxlem1  26569  irrapxlem2  26570  irrapxlem4  26572  pell1234qrreccl  26601  pell1234qrmulcl  26602  pell14qrgt0  26606  pell1234qrdich  26608  pell1qrgaplem  26620  pellqrex  26626  reglogltb  26638  reglogleb  26639  monotoddzzfi  26689  oddcomabszz  26691  jm2.24  26712  congsym  26717  acongtr  26727  acongrep  26729  jm2.18  26743  jm2.23  26751  jm2.26a  26755  jm2.26lem3  26756  jm2.27b  26761  rmydioph  26769  setindtr  26779  wepwsolem  26800  dnnumch1  26803  fnwe2lem2  26810  aomclem6  26818  dfac21  26826  islssfg  26830  lnmlsslnm  26841  pwslnm  26858  uvcff  26902  lindfmm  26959  islinds4  26967  lnrfg  26985  dgrsub2  27001  mpaaeu  27017  rngunsnply  27040  f1omvdconj  27051  f1otrspeq  27052  f1omvdco2  27053  symggen  27073  matassa  27143  acsfn1p  27169  cntzsdrg  27172  idomodle  27174  fmuldfeqlem1  27373  fmuldfeq  27374  climrec  27390  climinf  27393  climsuse  27395  itgsinexp  27410  stoweidlem3  27413  stoweidlem7  27417  stoweidlem14  27424  stoweidlem29  27439  stoweidlem34  27444  stoweidlem46  27456  2reu4a  27628  funressnfv  27654  2pthfrgra  27757  frgrancvvdeqlem3  27777  frgrancvvdeqlemC  27784  frgrancvvdeqlem9  27786  bnj1098  28485  bnj1118  28684  bnj1417  28741  cvrval5  29580  3dim0  29622  pmapglbx  29934  pclfinclN  30115  lhplt  30165  lhpexle1  30173  lhpocnle  30181  lhpjat1  30185  lhpjat2  30186  lhpj1  30187  lhpmcvr  30188  lhpmcvr2  30189  lhpm0atN  30194  lhpmat  30195  ltrnid  30300  trlcl  30329  trlle  30349  cdlemc4  30359  cdleme0cp  30379  cdleme0cq  30380  cdlemeulpq  30385  cdleme1b  30391  cdleme1  30392  cdleme2  30393  cdleme3b  30394  cdleme3c  30395  cdlemedb  30462  cdleme27a  30532  docaclN  31290  doca2N  31292  djajN  31303  dihglblem5apreN  31457
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