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  2243  ax11el  2244  tfindsg  4799  frsn  4907  sofld  5277  soex  5278  foun  5652  f1oprg  5677  fcof1o  5985  foeqcnvco  5986  f1eqcocnv  5987  caovord3  6219  curry1  6397  curry2  6400  f1o2ndf1  6413  mpt2xopxnop0  6425  smores2  6575  smo11  6585  smoord  6586  oesuclem  6728  oelim  6737  oaordi  6748  oaass  6763  odi  6781  omass  6782  oen0  6788  oelim2  6797  nnaordi  6820  eceqoveq  6968  resixpfo  7059  boxcutc  7064  xpdom2  7162  domunsncan  7167  omxpenlem  7168  mapen  7230  xpmapenlem  7233  mapdom2  7237  php3  7252  onomeneq  7255  fineqvlem  7282  xpfi  7337  fiint  7342  dffi3  7394  marypha1lem  7396  ordtypelem7  7449  wemaplem3  7473  brwdom2  7497  unxpwdom2  7512  cantnfle  7582  cantnflt  7583  r1pwss  7666  rankval3b  7708  carddomi2  7813  isinffi  7835  fidomtri  7836  acndom  7888  dfac9  7972  dfac12lem1  7979  dfac12lem2  7980  ackbij1lem16  8071  ackbij2lem3  8077  fictb  8081  cofsmo  8105  cfsmolem  8106  cfcof  8110  infpssrlem4  8142  fin23lem39  8186  isf32lem2  8190  isf32lem3  8191  fin1a2lem12  8247  fin1a2lem13  8248  fin12  8249  axdc3lem4  8289  axdc4lem  8291  ttukeylem3  8347  carden  8382  axrepnd  8425  canthwelem  8481  inawinalem  8520  gchina  8530  r1limwun  8567  inar1  8606  inatsk  8609  tskuni  8614  intgru  8645  nqereu  8762  ltexnq  8808  npex  8819  elnp  8820  prlem936  8880  recexsrlem  8934  mul02lem1  9198  lemul12a  9824  lediv12a  9859  lediv2a  9860  creur  9950  peano5nni  9959  nndiv  9996  rpnnen1lem1  10556  rpnnen1lem2  10557  rpnnen1lem3  10558  rpnnen1lem5  10560  xrmax2  10720  qextltlem  10744  xpncan  10786  xmulneg1  10804  xmulge0  10819  xlemul1a  10823  xrsupsslem  10841  xrinfmsslem  10842  xrub  10846  supxrun  10850  supxrunb1  10854  supxrunb2  10855  supxrbnd  10863  ixxub  10893  ixxlb  10894  elioc2  10929  elico2  10930  elicc2  10931  difreicc  10984  elfznelfzo  11147  modid  11225  seqf1olem1  11317  facndiv  11534  faclbnd  11536  bcval5  11564  hashdom  11608  hashfacen  11658  seqcoll  11667  brfi1indlem  11669  brfi1uzind  11670  revccat  11753  seqshft  11855  sqrmo  12012  absmax  12088  rexico  12112  cau3lem  12113  limsupval2  12229  rlim2lt  12246  o1lo1  12286  rlimconst  12293  climrlim2  12296  2clim  12321  rlimcn2  12339  reccn2  12345  cn1lem  12346  o1of2  12361  lo1const  12369  climsqz  12389  climsqz2  12390  isercolllem2  12414  isercoll  12416  climsup  12418  climcau  12419  caucvgrlem2  12423  iseralt  12433  sumeq2ii  12442  fsum2dlem  12509  fsum0diag2  12521  cvgcmp  12550  cvgcmpce  12552  climcnds  12586  divrcnv  12587  mertenslem1  12616  mertens  12618  efaddlem  12650  tanaddlem  12722  sqr2irr  12803  dvdseq  12852  dvdsext  12855  odd2np1  12863  bitsf1  12913  smuval2  12949  qredeq  13061  qredeu  13062  exprmfct  13065  isprm5  13067  rpexp1i  13076  nonsq  13106  iserodd  13164  pcz  13209  fldivp1  13221  pcfac  13223  expnprm  13226  prmpwdvds  13227  prmreclem5  13243  vdwapf  13295  vdwnnlem2  13319  0ramcl  13346  setscom  13452  firest  13615  isacs2  13833  mreacs  13838  acsfn  13839  acsfn1  13841  ressffth  14090  setcmon  14197  uncfcurf  14291  drsdirfi  14350  lubid  14394  resmhm  14714  resmhm2  14715  mhmco  14717  pwsdiagmhm  14723  gsumwsubmcl  14739  gsumwmhm  14745  gsumwspan  14746  isgrpinv  14810  mulgz  14866  resghm  14977  cntzsubm  15089  cntzmhm  15092  odf1  15153  gexdvds  15173  pgpfi  15194  sylow3lem6  15221  lsmub1x  15235  lsmless12  15250  efgred2  15340  efgcpbllemb  15342  torsubg  15424  prmcyg  15458  ghmcyg  15460  gsumval3  15469  dprdfadd  15533  subgdmdprd  15547  dprdsn  15549  dmdprdsplitlem  15550  dmdprdsplit2lem  15558  ablfacrp  15579  ablfac1b  15583  ablfac2  15602  mgpress  15614  irredrmul  15767  isdrng2  15800  drngmul0or  15811  issubdrg  15848  islss3  15990  lmhmco  16074  lmhmplusg  16075  pwsdiaglmhm  16088  lvecvs0or  16135  lbsextlem2  16186  2idlcpbl  16260  issubassa2  16358  coe1tmmul2  16623  coe1tmmul  16624  qsssubdrg  16713  prmirredlem  16728  mulgrhm2  16743  znidomb  16797  znunit  16799  cyggic  16808  pjfo  16897  obslbs  16912  tgdom  16998  fctop  17023  pptbas  17027  elcls3  17102  toponmre  17112  neiptopuni  17149  neiptoptop  17150  neiptopreu  17152  maxlp  17165  ssrest  17194  cnfval  17251  cnpfval  17252  iscnp3  17262  subbascn  17272  ssidcn  17273  cnpnei  17282  cncls2  17291  cncls  17292  cnntr  17293  cncnp  17298  restcnrm  17380  cmpsublem  17416  cmpsub  17417  cmpcld  17419  uncmp  17420  hauscmplem  17423  cmpfi  17425  iunconlem  17443  2ndcrest  17470  2ndcctbss  17471  2ndcomap  17474  2ndcsep  17475  1stcelcls  17477  lly1stc  17512  1stckgenlem  17538  ptval  17555  ptbasfi  17566  txcls  17589  tx1cn  17594  ptclsg  17600  xkoccn  17604  upxp  17608  xkococnlem  17644  imasnopn  17675  imasncld  17676  imasncls  17677  tgqtop  17697  qtopcld  17698  reghmph  17778  ptcmpfi  17798  filcon  17868  fbasrn  17869  filuni  17870  isufil2  17893  ssufl  17903  ufileu  17904  filufint  17905  ufilen  17915  rnelfm  17938  flimopn  17960  flimclsi  17963  hauspwpwf1  17972  isfcls  17994  fcfval  18018  alexsublem  18028  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALTlem4  18034  ptcmplem2  18037  ptcmplem3  18038  cnextfval  18046  symgtgp  18084  opnsubg  18090  clsnsg  18092  tsmsres  18126  tsmsf1o  18127  restutopopn  18221  neipcfilu  18279  stdbdmet  18499  metcnp  18524  metustidOLD  18542  metustid  18543  metustsymOLD  18544  metustblOLD  18563  metustbl  18564  metutopOLD  18565  psmetutop  18566  isngp2  18597  subgngp  18629  ngptgp  18630  tngtopn  18644  sranlm  18673  nlmvscn  18676  nmo0  18722  nmoco  18724  qdensere  18757  iocopnst  18918  oprpiece1res2  18930  evth2  18938  xlebnum  18943  lebnumii  18944  pcoass  19002  nmoleub2lem3  19076  nmhmcn  19081  lmnn  19169  cfilfcls  19180  iscmet3lem1  19197  iscmet3lem2  19198  causs  19204  equivcfil  19205  lmclim  19208  lmcau  19218  flimcfil  19219  cmetss  19220  relcmpcmet  19222  bcthlem4  19233  bcthlem5  19234  minveclem3  19283  ovoliunlem2  19352  ovolicc2lem4  19369  nulmbl2  19384  iundisj  19395  ioombl1lem4  19408  vitalilem1  19453  vitali  19458  mbfconstlem  19474  mbfimaicc  19478  mbfimaopnlem  19500  mbfsup  19509  i1fd  19526  i1fmullem  19539  i1fadd  19540  itg1addlem4  19544  itg1addlem5  19545  i1fres  19550  itg10a  19555  itg1climres  19559  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  itg2const2  19586  itg2seq  19587  itg2monolem1  19595  itg2mono  19598  itg2i1fseqle  19599  itg2cnlem1  19606  iblitg  19613  ibl0  19631  itgss  19656  itgeqa  19658  iblabsr  19674  iblmulc2  19675  bddmulibl  19683  dvnff  19762  dvcobr  19785  dvrec  19794  dvmptfsum  19812  dvexp3  19815  c1liplem1  19833  c1lip1  19834  dvgt0lem1  19839  evlslem3  19888  evlseu  19890  evlsval  19893  tdeglem4  19936  ply1divex  20012  q1pval  20029  fta1g  20043  plyco0  20064  plyeq0lem  20082  plymullem1  20086  plyco  20113  coemullem  20121  coemulhi  20125  coemulc  20126  coe1termlem  20129  dgrlt  20137  dgrco  20146  plycjlem  20147  dvply1  20154  plydivex  20167  fta1  20178  aalioulem2  20203  aalioulem3  20204  aalioulem6  20207  aaliou  20208  taylfval  20228  ulmcaulem  20263  ulmcau  20264  itgulm  20277  pserdvlem2  20297  pilem2  20321  divlogrlim  20479  logcnlem5  20490  advlogexp  20499  cxpcn3  20585  atantayl2  20731  leibpi  20735  birthdaylem3  20745  rlimcnp  20757  cxplim  20763  cxploglim2  20770  ftalem3  20810  basellem2  20817  mumullem1  20915  sqff1o  20918  muinv  20931  chtublem  20948  vmasum  20953  logfac2  20954  mersenne  20964  dchrptlem1  21001  bposlem1  21021  bposlem3  21023  bposlem5  21025  lgslem4  21036  lgsval2lem  21043  lgsmod  21058  lgsdir2lem4  21063  lgsdinn0  21077  lgsquad2lem2  21096  lgsquad3  21098  2sqlem6  21106  2sqlem7  21107  dchrisumlem3  21138  dchrmusumlema  21140  dchrmusum2  21141  dchrvmasumlem1  21142  dchrvmasum2lem  21143  dchrvmasumlem2  21145  dchrvmasumiflem1  21148  dchrisum0lema  21161  dchrisum0lem2a  21164  dchrisum0lem2  21165  mulog2sumlem2  21182  selberg  21195  pntsval2  21223  pntibnd  21240  pntlem3  21256  ostthlem1  21274  ostth2lem2  21281  ostth3  21285  usgrares1  21377  nbgraf1olem1  21404  nb3graprlem1  21413  cusgrasize2inds  21439  cusgrafilem2  21442  2wlklem1  21550  constr2wlk  21551  constr3trl  21599  constr3pth  21600  constr3cycl  21601  usgravd0nedg  21636  iseupa  21640  eupath2  21655  grpoidinv  21749  grpoideu  21750  nvmul0or  22086  vacn  22143  smcnlem  22146  nmoub3i  22227  nmoo0  22245  blocnilem  22258  ubthlem1  22325  ubthlem2  22326  ubthlem3  22327  minvecolem3  22331  hvmul0or  22480  hvmulcan  22527  hvaddsub4  22533  his35  22543  occon  22742  ocorth  22746  occl  22759  chscllem2  23093  5oalem1  23109  5oalem2  23110  3oalem2  23118  pjds3i  23168  nmopub2tALT  23365  nmfnleub2  23382  hmopadj2  23397  0cnop  23435  0cnfn  23436  nmophmi  23487  cnlnadjlem6  23528  leopnmid  23594  nmopleid  23595  opsqrlem1  23596  pjss2coi  23620  pjssdif1i  23631  pj3cor1i  23665  mdsl0  23766  mdslmd1lem1  23781  mdslmd1lem2  23782  csmdsymi  23790  superpos  23810  atomli  23838  chirredlem2  23847  chirredlem3  23848  atcvat3i  23852  atcvat4i  23853  mdsymlem5  23863  cdjreui  23888  cdj1i  23889  disjdifprg  23970  iundisjf  23982  xaddeq0  24072  iundisjfi  24105  ishashinf  24112  xrsmulgzz  24153  xrge0adddir  24168  ofldchr  24197  subofld  24198  xrge0iifiso  24274  pnfneige0  24289  lmxrge0  24290  gsumesum  24404  esumlub  24405  esumcst  24408  insiga  24473  measinb  24528  cntmeas  24533  imambfm  24565  rrvsum  24665  ballotlemsv  24720  ballotlemsima  24726  derangenlem  24810  subfacp1lem6  24824  conpcon  24875  txscon  24881  mulge0b  25144  ntrivcvg  25178  prodeq2ii  25192  fprod2dlem  25257  fundmpss  25336  dftrpred3g  25450  poseq  25467  soseq  25468  sltval2  25524  nobndlem6  25565  brbtwn2  25748  colinearalglem4  25752  colinearalg  25753  axsegconlem8  25767  axsegconlem9  25768  axsegconlem10  25769  ax5seglem3  25774  ax5seglem5  25776  axbtwnid  25782  axlowdimlem17  25801  axeuclid  25806  axcontlem2  25808  axcontlem7  25813  axcontlem8  25814  lxflflp1  26142  mblfinlem  26143  mblfinlem2  26144  ismblfin  26146  cnambfre  26154  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  iblabsnclem  26167  iblmulc2nc  26169  ftc1cnnc  26178  finminlem  26211  nn0prpwlem  26215  lfinpfin  26273  neibastop3  26281  fgmin  26289  filbcmb  26332  sdclem1  26337  fdc  26339  nnubfi  26344  nninfnub  26345  geomcau  26355  istotbnd3  26370  sstotbnd3  26375  isbnd3  26383  ssbnd  26387  prdsbnd  26392  cntotbnd  26395  heiborlem8  26417  bfplem2  26422  rrncmslem  26431  rngoisocnv  26487  unichnidl  26531  keridl  26532  prnc  26567  elrfirn  26639  isnacs3  26654  mzpsubmpt  26690  mzprename  26696  lzunuz  26716  eldiophss  26723  eqrabdioph  26726  rexrabdioph  26744  rabdiophlem2  26752  ctbnfien  26769  irrapxlem1  26775  irrapxlem2  26776  irrapxlem4  26778  pell1234qrreccl  26807  pell1234qrmulcl  26808  pell14qrgt0  26812  pell1234qrdich  26814  pell1qrgaplem  26826  pellqrex  26832  reglogltb  26844  reglogleb  26845  monotoddzzfi  26895  oddcomabszz  26897  jm2.24  26918  congsym  26923  acongtr  26933  acongrep  26935  jm2.18  26949  jm2.23  26957  jm2.26a  26961  jm2.26lem3  26962  jm2.27b  26967  rmydioph  26975  setindtr  26985  wepwsolem  27006  dnnumch1  27009  fnwe2lem2  27016  aomclem6  27024  dfac21  27032  islssfg  27036  lnmlsslnm  27047  pwslnm  27064  uvcff  27108  lindfmm  27165  islinds4  27173  lnrfg  27191  dgrsub2  27207  mpaaeu  27223  rngunsnply  27246  f1omvdconj  27257  f1otrspeq  27258  f1omvdco2  27259  symggen  27279  matassa  27349  acsfn1p  27375  cntzsdrg  27378  idomodle  27380  fmuldfeqlem1  27579  fmuldfeq  27580  climrec  27596  climinf  27599  climsuse  27601  itgsinexp  27616  stoweidlem3  27619  stoweidlem7  27623  stoweidlem14  27630  stoweidlem29  27645  stoweidlem34  27650  stoweidlem46  27662  2reu4a  27834  funressnfv  27859  swrdccat3a0  28015  swrdccatin2  28018  swrdccatin12lem3a  28021  swrdccat3b  28031  usgra2pthlem1  28040  el2spthonot0  28068  2pthfrgra  28115  frgrancvvdeqlem3  28135  frgrancvvdeqlemC  28142  frgrancvvdeqlem9  28144  frg2woteu  28158  frg2woteq  28163  bnj1098  28860  bnj1118  29059  bnj1417  29116  cvrval5  29897  3dim0  29939  pmapglbx  30251  pclfinclN  30432  lhplt  30482  lhpexle1  30490  lhpocnle  30498  lhpjat1  30502  lhpjat2  30503  lhpj1  30504  lhpmcvr  30505  lhpmcvr2  30506  lhpm0atN  30511  lhpmat  30512  ltrnid  30617  trlcl  30646  trlle  30666  cdlemc4  30676  cdleme0cp  30696  cdleme0cq  30697  cdlemeulpq  30702  cdleme1b  30708  cdleme1  30709  cdleme2  30710  cdleme3b  30711  cdleme3c  30712  cdlemedb  30779  cdleme27a  30849  docaclN  31607  doca2N  31609  djajN  31620  dihglblem5apreN  31774
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