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  2269  ax11el  2270  tfindsg  4831  frsn  4939  sofld  5309  soex  5310  foun  5684  f1oprg  5709  fcof1o  6017  foeqcnvco  6018  f1eqcocnv  6019  caovord3  6251  curry1  6429  curry2  6432  f1o2ndf1  6445  mpt2xopxnop0  6457  smores2  6607  smo11  6617  smoord  6618  oesuclem  6760  oelim  6769  oaordi  6780  oaass  6795  odi  6813  omass  6814  oen0  6820  oelim2  6829  nnaordi  6852  eceqoveq  7000  resixpfo  7091  boxcutc  7096  xpdom2  7194  domunsncan  7199  omxpenlem  7200  mapen  7262  xpmapenlem  7265  mapdom2  7269  php3  7284  onomeneq  7287  fineqvlem  7314  xpfi  7369  fiint  7374  dffi3  7427  marypha1lem  7429  ordtypelem7  7482  wemaplem3  7506  brwdom2  7530  unxpwdom2  7545  cantnfle  7615  cantnflt  7616  r1pwss  7699  rankval3b  7741  carddomi2  7846  isinffi  7868  fidomtri  7869  acndom  7921  dfac9  8005  dfac12lem1  8012  dfac12lem2  8013  ackbij1lem16  8104  ackbij2lem3  8110  fictb  8114  cofsmo  8138  cfsmolem  8139  cfcof  8143  infpssrlem4  8175  fin23lem39  8219  isf32lem2  8223  isf32lem3  8224  fin1a2lem12  8280  fin1a2lem13  8281  fin12  8282  axdc3lem4  8322  axdc4lem  8324  ttukeylem3  8380  carden  8415  axrepnd  8458  canthwelem  8514  inawinalem  8553  gchina  8563  r1limwun  8600  inar1  8639  inatsk  8642  tskuni  8647  intgru  8678  nqereu  8795  ltexnq  8841  npex  8852  elnp  8853  prlem936  8913  recexsrlem  8967  mul02lem1  9231  lemul12a  9857  lediv12a  9892  lediv2a  9893  creur  9983  peano5nni  9992  nndiv  10029  rpnnen1lem1  10589  rpnnen1lem2  10590  rpnnen1lem3  10591  rpnnen1lem5  10593  xrmax2  10753  qextltlem  10777  xpncan  10819  xmulneg1  10837  xmulge0  10852  xlemul1a  10856  xrsupsslem  10874  xrinfmsslem  10875  xrub  10879  supxrun  10883  supxrunb1  10887  supxrunb2  10888  supxrbnd  10896  ixxub  10926  ixxlb  10927  elioc2  10962  elico2  10963  elicc2  10964  difreicc  11017  elfznelfzo  11180  modid  11258  seqf1olem1  11350  facndiv  11567  faclbnd  11569  bcval5  11597  hashdom  11641  hashfacen  11691  seqcoll  11700  brfi1indlem  11702  brfi1uzind  11703  revccat  11786  seqshft  11888  sqrmo  12045  absmax  12121  rexico  12145  cau3lem  12146  limsupval2  12262  rlim2lt  12279  o1lo1  12319  rlimconst  12326  climrlim2  12329  2clim  12354  rlimcn2  12372  reccn2  12378  cn1lem  12379  o1of2  12394  lo1const  12402  climsqz  12422  climsqz2  12423  isercolllem2  12447  isercoll  12449  climsup  12451  climcau  12452  caucvgrlem2  12456  iseralt  12466  sumeq2ii  12475  fsum2dlem  12542  fsum0diag2  12554  cvgcmp  12583  cvgcmpce  12585  climcnds  12619  divrcnv  12620  mertenslem1  12649  mertens  12651  efaddlem  12683  tanaddlem  12755  sqr2irr  12836  dvdseq  12885  dvdsext  12888  odd2np1  12896  bitsf1  12946  smuval2  12982  qredeq  13094  qredeu  13095  exprmfct  13098  isprm5  13100  rpexp1i  13109  nonsq  13139  iserodd  13197  pcz  13242  fldivp1  13254  pcfac  13256  expnprm  13259  prmpwdvds  13260  prmreclem5  13276  vdwapf  13328  vdwnnlem2  13352  0ramcl  13379  setscom  13485  firest  13648  isacs2  13866  mreacs  13871  acsfn  13872  acsfn1  13874  ressffth  14123  setcmon  14230  uncfcurf  14324  drsdirfi  14383  lubid  14427  resmhm  14747  resmhm2  14748  mhmco  14750  pwsdiagmhm  14756  gsumwsubmcl  14772  gsumwmhm  14778  gsumwspan  14779  isgrpinv  14843  mulgz  14899  resghm  15010  cntzsubm  15122  cntzmhm  15125  odf1  15186  gexdvds  15206  pgpfi  15227  sylow3lem6  15254  lsmub1x  15268  lsmless12  15283  efgred2  15373  efgcpbllemb  15375  torsubg  15457  prmcyg  15491  ghmcyg  15493  gsumval3  15502  dprdfadd  15566  subgdmdprd  15580  dprdsn  15582  dmdprdsplitlem  15583  dmdprdsplit2lem  15591  ablfacrp  15612  ablfac1b  15616  ablfac2  15635  mgpress  15647  irredrmul  15800  isdrng2  15833  drngmul0or  15844  issubdrg  15881  islss3  16023  lmhmco  16107  lmhmplusg  16108  pwsdiaglmhm  16121  lvecvs0or  16168  lbsextlem2  16219  2idlcpbl  16293  issubassa2  16391  coe1tmmul2  16656  coe1tmmul  16657  qsssubdrg  16746  prmirredlem  16761  mulgrhm2  16776  znidomb  16830  znunit  16832  cyggic  16841  pjfo  16930  obslbs  16945  tgdom  17031  fctop  17056  pptbas  17060  elcls3  17135  toponmre  17145  neiptopuni  17182  neiptoptop  17183  neiptopreu  17185  maxlp  17199  ssrest  17228  cnfval  17285  cnpfval  17286  iscnp3  17296  subbascn  17306  ssidcn  17307  cnpnei  17316  cncls2  17325  cncls  17326  cnntr  17327  cncnp  17332  restcnrm  17414  cmpsublem  17450  cmpsub  17451  cmpcld  17453  uncmp  17454  hauscmplem  17457  cmpfi  17459  iunconlem  17478  2ndcrest  17505  2ndcctbss  17506  2ndcomap  17509  2ndcsep  17510  1stcelcls  17512  lly1stc  17547  1stckgenlem  17573  ptval  17590  ptbasfi  17601  txcls  17624  tx1cn  17629  ptclsg  17635  xkoccn  17639  upxp  17643  xkococnlem  17679  imasnopn  17710  imasncld  17711  imasncls  17712  tgqtop  17732  qtopcld  17733  reghmph  17813  ptcmpfi  17833  filcon  17903  fbasrn  17904  filuni  17905  isufil2  17928  ssufl  17938  ufileu  17939  filufint  17940  ufilen  17950  rnelfm  17973  flimopn  17995  flimclsi  17998  hauspwpwf1  18007  isfcls  18029  fcfval  18053  alexsublem  18063  alexsubALTlem2  18067  alexsubALTlem3  18068  alexsubALTlem4  18069  ptcmplem2  18072  ptcmplem3  18073  cnextfval  18081  symgtgp  18119  opnsubg  18125  clsnsg  18127  tsmsres  18161  tsmsf1o  18162  restutopopn  18256  neipcfilu  18314  stdbdmet  18534  metcnp  18559  metustidOLD  18577  metustid  18578  metustsymOLD  18579  metustblOLD  18598  metustbl  18599  metutopOLD  18600  psmetutop  18601  isngp2  18632  subgngp  18664  ngptgp  18665  tngtopn  18679  sranlm  18708  nlmvscn  18711  nmo0  18757  nmoco  18759  qdensere  18792  iocopnst  18953  oprpiece1res2  18965  evth2  18973  xlebnum  18978  lebnumii  18979  pcoass  19037  nmoleub2lem3  19111  nmhmcn  19116  lmnn  19204  cfilfcls  19215  iscmet3lem1  19232  iscmet3lem2  19233  causs  19239  equivcfil  19240  lmclim  19243  lmcau  19253  flimcfil  19254  cmetss  19255  relcmpcmet  19257  bcthlem4  19268  bcthlem5  19269  minveclem3  19318  ovoliunlem2  19387  ovolicc2lem4  19404  nulmbl2  19419  iundisj  19430  ioombl1lem4  19443  vitalilem1  19488  vitali  19493  mbfconstlem  19509  mbfimaicc  19513  mbfimaopnlem  19535  mbfsup  19544  i1fd  19561  i1fmullem  19574  i1fadd  19575  itg1addlem4  19579  itg1addlem5  19580  i1fres  19585  itg10a  19590  itg1climres  19594  mbfi1fseqlem3  19597  mbfi1fseqlem4  19598  mbfi1fseqlem5  19599  itg2const2  19621  itg2seq  19622  itg2monolem1  19630  itg2mono  19633  itg2i1fseqle  19634  itg2cnlem1  19641  iblitg  19648  ibl0  19666  itgss  19691  itgeqa  19693  iblabsr  19709  iblmulc2  19710  bddmulibl  19718  dvnff  19797  dvcobr  19820  dvrec  19829  dvmptfsum  19847  dvexp3  19850  c1liplem1  19868  c1lip1  19869  dvgt0lem1  19874  evlslem3  19923  evlseu  19925  evlsval  19928  tdeglem4  19971  ply1divex  20047  q1pval  20064  fta1g  20078  plyco0  20099  plyeq0lem  20117  plymullem1  20121  plyco  20148  coemullem  20156  coemulhi  20160  coemulc  20161  coe1termlem  20164  dgrlt  20172  dgrco  20181  plycjlem  20182  dvply1  20189  plydivex  20202  fta1  20213  aalioulem2  20238  aalioulem3  20239  aalioulem6  20242  aaliou  20243  taylfval  20263  ulmcaulem  20298  ulmcau  20299  itgulm  20312  pserdvlem2  20332  pilem2  20356  divlogrlim  20514  logcnlem5  20525  advlogexp  20534  cxpcn3  20620  atantayl2  20766  leibpi  20770  birthdaylem3  20780  rlimcnp  20792  cxplim  20798  cxploglim2  20805  ftalem3  20845  basellem2  20852  mumullem1  20950  sqff1o  20953  muinv  20966  chtublem  20983  vmasum  20988  logfac2  20989  mersenne  20999  dchrptlem1  21036  bposlem1  21056  bposlem3  21058  bposlem5  21060  lgslem4  21071  lgsval2lem  21078  lgsmod  21093  lgsdir2lem4  21098  lgsdinn0  21112  lgsquad2lem2  21131  lgsquad3  21133  2sqlem6  21141  2sqlem7  21142  dchrisumlem3  21173  dchrmusumlema  21175  dchrmusum2  21176  dchrvmasumlem1  21177  dchrvmasum2lem  21178  dchrvmasumlem2  21180  dchrvmasumiflem1  21183  dchrisum0lema  21196  dchrisum0lem2a  21199  dchrisum0lem2  21200  mulog2sumlem2  21217  selberg  21230  pntsval2  21258  pntibnd  21275  pntlem3  21291  ostthlem1  21309  ostth2lem2  21316  ostth3  21320  usgrares1  21412  nbgraf1olem1  21439  nb3graprlem1  21448  cusgrasize2inds  21474  cusgrafilem2  21477  2wlklem1  21585  constr2wlk  21586  constr3trl  21634  constr3pth  21635  constr3cycl  21636  usgravd0nedg  21671  iseupa  21675  eupath2  21690  grpoidinv  21784  grpoideu  21785  nvmul0or  22121  vacn  22178  smcnlem  22181  nmoub3i  22262  nmoo0  22280  blocnilem  22293  ubthlem1  22360  ubthlem2  22361  ubthlem3  22362  minvecolem3  22366  hvmul0or  22515  hvmulcan  22562  hvaddsub4  22568  his35  22578  occon  22777  ocorth  22781  occl  22794  chscllem2  23128  5oalem1  23144  5oalem2  23145  3oalem2  23153  pjds3i  23203  nmopub2tALT  23400  nmfnleub2  23417  hmopadj2  23432  0cnop  23470  0cnfn  23471  nmophmi  23522  cnlnadjlem6  23563  leopnmid  23629  nmopleid  23630  opsqrlem1  23631  pjss2coi  23655  pjssdif1i  23666  pj3cor1i  23700  mdsl0  23801  mdslmd1lem1  23816  mdslmd1lem2  23817  csmdsymi  23825  superpos  23845  atomli  23873  chirredlem2  23882  chirredlem3  23883  atcvat3i  23887  atcvat4i  23888  mdsymlem5  23898  cdjreui  23923  cdj1i  23924  disjdifprg  24005  iundisjf  24017  xaddeq0  24107  iundisjfi  24140  ishashinf  24147  xrsmulgzz  24188  xrge0adddir  24203  ofldchr  24232  subofld  24233  xrge0iifiso  24309  pnfneige0  24324  lmxrge0  24325  gsumesum  24439  esumlub  24440  esumcst  24443  insiga  24508  measinb  24563  cntmeas  24568  imambfm  24600  rrvsum  24700  ballotlemsv  24755  ballotlemsima  24761  derangenlem  24845  subfacp1lem6  24859  conpcon  24910  txscon  24916  mulge0b  25179  ntrivcvg  25214  prodeq2ii  25228  fprod2dlem  25293  fundmpss  25377  dftrpred3g  25491  poseq  25508  soseq  25509  sltval2  25565  nobndlem6  25606  brbtwn2  25792  colinearalglem4  25796  colinearalg  25797  axsegconlem8  25811  axsegconlem9  25812  axsegconlem10  25813  ax5seglem3  25818  ax5seglem5  25820  axbtwnid  25826  axlowdimlem17  25845  axeuclid  25850  axcontlem2  25852  axcontlem7  25857  axcontlem8  25858  lxflflp1  26189  mblfinlem  26190  mblfinlem2  26191  ismblfin  26193  cnambfre  26201  itg2addnclem  26202  itg2addnclem2  26203  itg2addnclem3  26204  itg2addnc  26205  itg2gt0cn  26206  iblabsnclem  26214  iblmulc2nc  26216  ftc1cnnc  26225  finminlem  26258  nn0prpwlem  26262  lfinpfin  26320  neibastop3  26328  fgmin  26336  filbcmb  26379  sdclem1  26384  fdc  26386  nnubfi  26391  nninfnub  26392  geomcau  26402  istotbnd3  26417  sstotbnd3  26422  isbnd3  26430  ssbnd  26434  prdsbnd  26439  cntotbnd  26442  heiborlem8  26464  bfplem2  26469  rrncmslem  26478  rngoisocnv  26534  unichnidl  26578  keridl  26579  prnc  26614  elrfirn  26686  isnacs3  26701  mzpsubmpt  26737  mzprename  26743  lzunuz  26763  eldiophss  26770  eqrabdioph  26773  rexrabdioph  26791  rabdiophlem2  26799  ctbnfien  26816  irrapxlem1  26822  irrapxlem2  26823  irrapxlem4  26825  pell1234qrreccl  26854  pell1234qrmulcl  26855  pell14qrgt0  26859  pell1234qrdich  26861  pell1qrgaplem  26873  pellqrex  26879  reglogltb  26891  reglogleb  26892  monotoddzzfi  26942  oddcomabszz  26944  jm2.24  26965  congsym  26970  acongtr  26980  acongrep  26982  jm2.18  26996  jm2.23  27004  jm2.26a  27008  jm2.26lem3  27009  jm2.27b  27014  rmydioph  27022  setindtr  27032  wepwsolem  27053  dnnumch1  27056  fnwe2lem2  27063  aomclem6  27071  dfac21  27079  islssfg  27083  lnmlsslnm  27094  pwslnm  27111  uvcff  27155  lindfmm  27212  islinds4  27220  lnrfg  27238  dgrsub2  27254  mpaaeu  27270  rngunsnply  27293  f1omvdconj  27304  f1otrspeq  27305  f1omvdco2  27306  symggen  27326  matassa  27396  acsfn1p  27422  cntzsdrg  27425  idomodle  27427  fmuldfeqlem1  27626  fmuldfeq  27627  climrec  27643  climinf  27646  climsuse  27648  itgsinexp  27663  stoweidlem3  27666  stoweidlem7  27670  stoweidlem14  27677  stoweidlem29  27692  stoweidlem34  27697  stoweidlem46  27709  2reu4a  27881  funressnfv  27906  swrdccat3a0  28090  swrdccatin2  28093  swrdccatin12lem3a  28096  swrdccat3b  28106  2shwrd1lem2  28137  2shwrd2lem1  28142  2shwrd2lem3  28144  shwrdssizelem1a  28165  shwrdssizelem3  28168  usgra2pthlem1  28184  el2spthonot0  28212  2pthfrgra  28259  frgrancvvdeqlem3  28279  frgrancvvdeqlemC  28286  frgrancvvdeqlem9  28288  frg2woteu  28302  frg2woteq  28307  bnj1098  29008  bnj1118  29207  bnj1417  29264  cvrval5  30051  3dim0  30093  pmapglbx  30405  pclfinclN  30586  lhplt  30636  lhpexle1  30644  lhpocnle  30652  lhpjat1  30656  lhpjat2  30657  lhpj1  30658  lhpmcvr  30659  lhpmcvr2  30660  lhpm0atN  30665  lhpmat  30666  ltrnid  30771  trlcl  30800  trlle  30820  cdlemc4  30830  cdleme0cp  30850  cdleme0cq  30851  cdlemeulpq  30856  cdleme1b  30862  cdleme1  30863  cdleme2  30864  cdleme3b  30865  cdleme3c  30866  cdlemedb  30933  cdleme27a  31003  docaclN  31761  doca2N  31763  djajN  31774  dihglblem5apreN  31928
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