MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ad2antlr Structured version   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  2269  ax11el  2270  tfindsg  4832  frsn  4940  sofld  5310  soex  5311  foun  5685  f1oprg  5710  fcof1o  6018  foeqcnvco  6019  f1eqcocnv  6020  caovord3  6252  curry1  6430  curry2  6433  f1o2ndf1  6446  mpt2xopxnop0  6458  smores2  6608  smo11  6618  smoord  6619  oesuclem  6761  oelim  6770  oaordi  6781  oaass  6796  odi  6814  omass  6815  oen0  6821  oelim2  6830  nnaordi  6853  eceqoveq  7001  resixpfo  7092  boxcutc  7097  xpdom2  7195  domunsncan  7200  omxpenlem  7201  mapen  7263  xpmapenlem  7266  mapdom2  7270  php3  7285  onomeneq  7288  fineqvlem  7315  xpfi  7370  fiint  7375  dffi3  7428  marypha1lem  7430  ordtypelem7  7485  wemaplem3  7509  brwdom2  7533  unxpwdom2  7548  cantnfle  7618  cantnflt  7619  r1pwss  7702  rankval3b  7744  carddomi2  7849  isinffi  7871  fidomtri  7872  acndom  7924  dfac9  8008  dfac12lem1  8015  dfac12lem2  8016  ackbij1lem16  8107  ackbij2lem3  8113  fictb  8117  cofsmo  8141  cfsmolem  8142  cfcof  8146  infpssrlem4  8178  fin23lem39  8222  isf32lem2  8226  isf32lem3  8227  fin1a2lem12  8283  fin1a2lem13  8284  fin12  8285  axdc3lem4  8325  axdc4lem  8327  ttukeylem3  8383  carden  8418  axrepnd  8461  canthwelem  8517  inawinalem  8556  gchina  8566  r1limwun  8603  inar1  8642  inatsk  8645  tskuni  8650  intgru  8681  nqereu  8798  ltexnq  8844  npex  8855  elnp  8856  prlem936  8916  recexsrlem  8970  mul02lem1  9234  lemul12a  9860  lediv12a  9895  lediv2a  9896  creur  9986  peano5nni  9995  nndiv  10032  rpnnen1lem1  10592  rpnnen1lem2  10593  rpnnen1lem3  10594  rpnnen1lem5  10596  xrmax2  10756  qextltlem  10780  xpncan  10822  xmulneg1  10840  xmulge0  10855  xlemul1a  10859  xrsupsslem  10877  xrinfmsslem  10878  xrub  10882  supxrun  10886  supxrunb1  10890  supxrunb2  10891  supxrbnd  10899  ixxub  10929  ixxlb  10930  elioc2  10965  elico2  10966  elicc2  10967  difreicc  11020  elfznelfzo  11184  modid  11262  seqf1olem1  11354  facndiv  11571  faclbnd  11573  bcval5  11601  hashdom  11645  hashfacen  11695  seqcoll  11704  brfi1indlem  11706  brfi1uzind  11707  revccat  11790  seqshft  11892  sqrmo  12049  absmax  12125  rexico  12149  cau3lem  12150  limsupval2  12266  rlim2lt  12283  o1lo1  12323  rlimconst  12330  climrlim2  12333  2clim  12358  rlimcn2  12376  reccn2  12382  cn1lem  12383  o1of2  12398  lo1const  12406  climsqz  12426  climsqz2  12427  isercolllem2  12451  isercoll  12453  climsup  12455  climcau  12456  caucvgrlem2  12460  iseralt  12470  sumeq2ii  12479  fsum2dlem  12546  fsum0diag2  12558  cvgcmp  12587  cvgcmpce  12589  climcnds  12623  divrcnv  12624  mertenslem1  12653  mertens  12655  efaddlem  12687  tanaddlem  12759  sqr2irr  12840  dvdseq  12889  dvdsext  12892  odd2np1  12900  bitsf1  12950  smuval2  12986  qredeq  13098  qredeu  13099  exprmfct  13102  isprm5  13104  rpexp1i  13113  nonsq  13143  iserodd  13201  pcz  13246  fldivp1  13258  pcfac  13260  expnprm  13263  prmpwdvds  13264  prmreclem5  13280  vdwapf  13332  vdwnnlem2  13356  0ramcl  13383  setscom  13489  firest  13652  isacs2  13870  mreacs  13875  acsfn  13876  acsfn1  13878  ressffth  14127  setcmon  14234  uncfcurf  14328  drsdirfi  14387  lubid  14431  resmhm  14751  resmhm2  14752  mhmco  14754  pwsdiagmhm  14760  gsumwsubmcl  14776  gsumwmhm  14782  gsumwspan  14783  isgrpinv  14847  mulgz  14903  resghm  15014  cntzsubm  15126  cntzmhm  15129  odf1  15190  gexdvds  15210  pgpfi  15231  sylow3lem6  15258  lsmub1x  15272  lsmless12  15287  efgred2  15377  efgcpbllemb  15379  torsubg  15461  prmcyg  15495  ghmcyg  15497  gsumval3  15506  dprdfadd  15570  subgdmdprd  15584  dprdsn  15586  dmdprdsplitlem  15587  dmdprdsplit2lem  15595  ablfacrp  15616  ablfac1b  15620  ablfac2  15639  mgpress  15651  irredrmul  15804  isdrng2  15837  drngmul0or  15848  issubdrg  15885  islss3  16027  lmhmco  16111  lmhmplusg  16112  pwsdiaglmhm  16125  lvecvs0or  16172  lbsextlem2  16223  2idlcpbl  16297  issubassa2  16395  coe1tmmul2  16660  coe1tmmul  16661  qsssubdrg  16750  prmirredlem  16765  mulgrhm2  16780  znidomb  16834  znunit  16836  cyggic  16845  pjfo  16934  obslbs  16949  tgdom  17035  fctop  17060  pptbas  17064  elcls3  17139  toponmre  17149  neiptopuni  17186  neiptoptop  17187  neiptopreu  17189  maxlp  17203  ssrest  17232  cnfval  17289  cnpfval  17290  iscnp3  17300  subbascn  17310  ssidcn  17311  cnpnei  17320  cncls2  17329  cncls  17330  cnntr  17331  cncnp  17336  restcnrm  17418  cmpsublem  17454  cmpsub  17455  cmpcld  17457  uncmp  17458  hauscmplem  17461  cmpfi  17463  iunconlem  17482  2ndcrest  17509  2ndcctbss  17510  2ndcomap  17513  2ndcsep  17514  1stcelcls  17516  lly1stc  17551  1stckgenlem  17577  ptval  17594  ptbasfi  17605  txcls  17628  tx1cn  17633  ptclsg  17639  xkoccn  17643  upxp  17647  xkococnlem  17683  imasnopn  17714  imasncld  17715  imasncls  17716  tgqtop  17736  qtopcld  17737  reghmph  17817  ptcmpfi  17837  filcon  17907  fbasrn  17908  filuni  17909  isufil2  17932  ssufl  17942  ufileu  17943  filufint  17944  ufilen  17954  rnelfm  17977  flimopn  17999  flimclsi  18002  hauspwpwf1  18011  isfcls  18033  fcfval  18057  alexsublem  18067  alexsubALTlem2  18071  alexsubALTlem3  18072  alexsubALTlem4  18073  ptcmplem2  18076  ptcmplem3  18077  cnextfval  18085  symgtgp  18123  opnsubg  18129  clsnsg  18131  tsmsres  18165  tsmsf1o  18166  restutopopn  18260  neipcfilu  18318  stdbdmet  18538  metcnp  18563  metustidOLD  18581  metustid  18582  metustsymOLD  18583  metustblOLD  18602  metustbl  18603  metutopOLD  18604  psmetutop  18605  isngp2  18636  subgngp  18668  ngptgp  18669  tngtopn  18683  sranlm  18712  nlmvscn  18715  nmo0  18761  nmoco  18763  qdensere  18796  iocopnst  18957  oprpiece1res2  18969  evth2  18977  xlebnum  18982  lebnumii  18983  pcoass  19041  nmoleub2lem3  19115  nmhmcn  19120  lmnn  19208  cfilfcls  19219  iscmet3lem1  19236  iscmet3lem2  19237  causs  19243  equivcfil  19244  lmclim  19247  lmcau  19257  flimcfil  19258  cmetss  19259  relcmpcmet  19261  bcthlem4  19272  bcthlem5  19273  minveclem3  19322  ovoliunlem2  19391  ovolicc2lem4  19408  nulmbl2  19423  iundisj  19434  ioombl1lem4  19447  vitalilem1  19492  vitali  19497  mbfconstlem  19513  mbfimaicc  19517  mbfimaopnlem  19539  mbfsup  19548  i1fd  19565  i1fmullem  19578  i1fadd  19579  itg1addlem4  19583  itg1addlem5  19584  i1fres  19589  itg10a  19594  itg1climres  19598  mbfi1fseqlem3  19601  mbfi1fseqlem4  19602  mbfi1fseqlem5  19603  itg2const2  19625  itg2seq  19626  itg2monolem1  19634  itg2mono  19637  itg2i1fseqle  19638  itg2cnlem1  19645  iblitg  19652  ibl0  19670  itgss  19695  itgeqa  19697  iblabsr  19713  iblmulc2  19714  bddmulibl  19722  dvnff  19801  dvcobr  19824  dvrec  19833  dvmptfsum  19851  dvexp3  19854  c1liplem1  19872  c1lip1  19873  dvgt0lem1  19878  evlslem3  19927  evlseu  19929  evlsval  19932  tdeglem4  19975  ply1divex  20051  q1pval  20068  fta1g  20082  plyco0  20103  plyeq0lem  20121  plymullem1  20125  plyco  20152  coemullem  20160  coemulhi  20164  coemulc  20165  coe1termlem  20168  dgrlt  20176  dgrco  20185  plycjlem  20186  dvply1  20193  plydivex  20206  fta1  20217  aalioulem2  20242  aalioulem3  20243  aalioulem6  20246  aaliou  20247  taylfval  20267  ulmcaulem  20302  ulmcau  20303  itgulm  20316  pserdvlem2  20336  pilem2  20360  divlogrlim  20518  logcnlem5  20529  advlogexp  20538  cxpcn3  20624  atantayl2  20770  leibpi  20774  birthdaylem3  20784  rlimcnp  20796  cxplim  20802  cxploglim2  20809  ftalem3  20849  basellem2  20856  mumullem1  20954  sqff1o  20957  muinv  20970  chtublem  20987  vmasum  20992  logfac2  20993  mersenne  21003  dchrptlem1  21040  bposlem1  21060  bposlem3  21062  bposlem5  21064  lgslem4  21075  lgsval2lem  21082  lgsmod  21097  lgsdir2lem4  21102  lgsdinn0  21116  lgsquad2lem2  21135  lgsquad3  21137  2sqlem6  21145  2sqlem7  21146  dchrisumlem3  21177  dchrmusumlema  21179  dchrmusum2  21180  dchrvmasumlem1  21181  dchrvmasum2lem  21182  dchrvmasumlem2  21184  dchrvmasumiflem1  21187  dchrisum0lema  21200  dchrisum0lem2a  21203  dchrisum0lem2  21204  mulog2sumlem2  21221  selberg  21234  pntsval2  21262  pntibnd  21279  pntlem3  21295  ostthlem1  21313  ostth2lem2  21320  ostth3  21324  usgrares1  21416  nbgraf1olem1  21443  nb3graprlem1  21452  cusgrasize2inds  21478  cusgrafilem2  21481  2wlklem1  21589  constr2wlk  21590  constr3trl  21638  constr3pth  21639  constr3cycl  21640  usgravd0nedg  21675  iseupa  21679  eupath2  21694  grpoidinv  21788  grpoideu  21789  nvmul0or  22125  vacn  22182  smcnlem  22185  nmoub3i  22266  nmoo0  22284  blocnilem  22297  ubthlem1  22364  ubthlem2  22365  ubthlem3  22366  minvecolem3  22370  hvmul0or  22519  hvmulcan  22566  hvaddsub4  22572  his35  22582  occon  22781  ocorth  22785  occl  22798  chscllem2  23132  5oalem1  23148  5oalem2  23149  3oalem2  23157  pjds3i  23207  nmopub2tALT  23404  nmfnleub2  23421  hmopadj2  23436  0cnop  23474  0cnfn  23475  nmophmi  23526  cnlnadjlem6  23567  leopnmid  23633  nmopleid  23634  opsqrlem1  23635  pjss2coi  23659  pjssdif1i  23670  pj3cor1i  23704  mdsl0  23805  mdslmd1lem1  23820  mdslmd1lem2  23821  csmdsymi  23829  superpos  23849  atomli  23877  chirredlem2  23886  chirredlem3  23887  atcvat3i  23891  atcvat4i  23892  mdsymlem5  23902  cdjreui  23927  cdj1i  23928  disjdifprg  24009  iundisjf  24021  xaddeq0  24111  iundisjfi  24144  ishashinf  24151  xrsmulgzz  24192  xrge0adddir  24207  ofldchr  24236  subofld  24237  xrge0iifiso  24313  pnfneige0  24328  lmxrge0  24329  gsumesum  24443  esumlub  24444  esumcst  24447  insiga  24512  measinb  24567  cntmeas  24572  imambfm  24604  rrvsum  24704  ballotlemsv  24759  ballotlemsima  24765  derangenlem  24849  subfacp1lem6  24863  conpcon  24914  txscon  24920  mulge0b  25183  ntrivcvg  25217  prodeq2ii  25231  fprod2dlem  25296  fundmpss  25382  dftrpred3g  25503  poseq  25520  soseq  25521  sltval2  25603  nobndlem6  25644  brbtwn2  25836  colinearalglem4  25840  colinearalg  25841  axsegconlem8  25855  axsegconlem9  25856  axsegconlem10  25857  ax5seglem3  25862  ax5seglem5  25864  axbtwnid  25870  axlowdimlem17  25889  axeuclid  25894  axcontlem2  25896  axcontlem7  25901  axcontlem8  25902  lxflflp1  26233  mblfinlem  26234  mblfinlem2  26235  ismblfin  26237  cnambfre  26245  itg2addnclem  26246  itg2addnclem2  26247  itg2addnclem3  26248  itg2addnc  26249  itg2gt0cn  26250  iblabsnclem  26258  iblmulc2nc  26260  ftc1cnnc  26269  ftc1anclem5  26274  ftc1anclem6  26275  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  finminlem  26312  nn0prpwlem  26316  lfinpfin  26374  neibastop3  26382  fgmin  26390  filbcmb  26433  sdclem1  26438  fdc  26440  nnubfi  26445  nninfnub  26446  geomcau  26456  istotbnd3  26471  sstotbnd3  26476  isbnd3  26484  ssbnd  26488  prdsbnd  26493  cntotbnd  26496  heiborlem8  26518  bfplem2  26523  rrncmslem  26532  rngoisocnv  26588  unichnidl  26632  keridl  26633  prnc  26668  elrfirn  26740  isnacs3  26755  mzpsubmpt  26791  mzprename  26797  lzunuz  26817  eldiophss  26824  eqrabdioph  26827  rexrabdioph  26845  rabdiophlem2  26853  ctbnfien  26870  irrapxlem1  26876  irrapxlem2  26877  irrapxlem4  26879  pell1234qrreccl  26908  pell1234qrmulcl  26909  pell14qrgt0  26913  pell1234qrdich  26915  pell1qrgaplem  26927  pellqrex  26933  reglogltb  26945  reglogleb  26946  monotoddzzfi  26996  oddcomabszz  26998  jm2.24  27019  congsym  27024  acongtr  27034  acongrep  27036  jm2.18  27050  jm2.23  27058  jm2.26a  27062  jm2.26lem3  27063  jm2.27b  27068  rmydioph  27076  setindtr  27086  wepwsolem  27107  dnnumch1  27110  fnwe2lem2  27117  aomclem6  27125  dfac21  27132  islssfg  27136  lnmlsslnm  27147  pwslnm  27164  uvcff  27208  lindfmm  27265  islinds4  27273  lnrfg  27291  dgrsub2  27307  mpaaeu  27323  rngunsnply  27346  f1omvdconj  27357  f1otrspeq  27358  f1omvdco2  27359  symggen  27379  matassa  27449  acsfn1p  27475  cntzsdrg  27478  idomodle  27480  fmuldfeqlem1  27679  fmuldfeq  27680  climrec  27696  climinf  27699  climsuse  27701  itgsinexp  27716  stoweidlem3  27719  stoweidlem7  27723  stoweidlem14  27730  stoweidlem29  27745  stoweidlem34  27750  stoweidlem46  27762  2reu4a  27934  funressnfv  27959  swrdccat3  28181  2cshw1lem2  28215  2cshwmod  28223  cshwssizelem1a  28242  cshwssizelem3  28245  cshwsexa  28254  usgra2pthlem1  28263  el2spthonot0  28291  2pthfrgra  28338  frgrancvvdeqlem3  28358  frgrancvvdeqlemC  28365  frgrancvvdeqlem9  28367  frg2woteu  28381  frg2woteq  28386  bnj1098  29091  bnj1118  29290  bnj1417  29347  cvrval5  30149  3dim0  30191  pmapglbx  30503  pclfinclN  30684  lhplt  30734  lhpexle1  30742  lhpocnle  30750  lhpjat1  30754  lhpjat2  30755  lhpj1  30756  lhpmcvr  30757  lhpmcvr2  30758  lhpm0atN  30763  lhpmat  30764  ltrnid  30869  trlcl  30898  trlle  30918  cdlemc4  30928  cdleme0cp  30948  cdleme0cq  30949  cdlemeulpq  30954  cdleme1b  30960  cdleme1  30961  cdleme2  30962  cdleme3b  30963  cdleme3c  30964  cdlemedb  31031  cdleme27a  31101  docaclN  31859  doca2N  31861  djajN  31872  dihglblem5apreN  32026
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