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

Theorem ad2antlr 726
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 465 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantll 713 1  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ad3antlr  730  simplr  754  simplrl  759  simplrr  760  ax12eq  2264  ax12el  2265  frsn  5076  sofld  5461  foun  5840  f1oprg  5862  fvreseq1  5989  foeqcnvco  6202  f1eqcocnv  6203  caovord3  6483  tfindsg  6690  soex  6738  curry1  6887  curry2  6890  f1o2ndf1  6903  suppfnss  6937  mpt2xopxnop0  6955  smores2  7037  smo11  7047  smoord  7048  oesuclem  7187  oelim  7196  oaordi  7207  oaass  7222  odi  7240  omass  7241  oen0  7247  oelim2  7256  nnaordi  7279  eceqoveq  7428  resixpfo  7519  boxcutc  7524  xpdom2  7624  domunsncan  7629  omxpenlem  7630  mapen  7693  xpmapenlem  7696  mapdom2  7700  php3  7715  onomeneq  7719  fineqvlem  7746  xpfi  7803  fiint  7809  dffi3  7903  marypha1lem  7905  ordtypelem7  7961  wemaplem3  7985  brwdom2  8011  unxpwdom2  8026  cantnfle  8102  cantnflt  8103  cantnfleOLD  8132  cantnfltOLD  8133  r1pwss  8214  rankval3b  8256  carddomi2  8363  isinffi  8385  fidomtri  8386  acndom  8444  dfac9  8528  dfac12lem1  8535  dfac12lem2  8536  ackbij1lem16  8627  ackbij2lem3  8633  fictb  8637  cofsmo  8661  cfsmolem  8662  cfcof  8666  infpssrlem4  8698  fin23lem39  8742  isf32lem2  8746  isf32lem3  8747  fin1a2lem12  8803  fin1a2lem13  8804  fin12  8805  axdc3lem4  8845  axdc4lem  8847  ttukeylem3  8903  carden  8938  axrepnd  8981  canthwelem  9040  inawinalem  9079  gchina  9089  r1limwun  9126  inar1  9165  inatsk  9168  tskuni  9173  intgru  9204  nqereu  9319  ltexnq  9365  npex  9376  elnp  9377  prlem936  9437  recexsrlem  9492  mul02lem1  9767  lemul12a  10412  mulge0b  10424  lediv12a  10450  lediv2a  10451  creur  10542  peano5nni  10551  nndiv  10588  rpnnen1lem1  11220  rpnnen1lem2  11221  rpnnen1lem3  11222  rpnnen1lem5  11224  xrmax2  11389  qextltlem  11413  xpncan  11455  xmulneg1  11473  xmulge0  11488  xlemul1a  11492  xrsupsslem  11510  xrinfmsslem  11511  xrub  11515  supxrun  11519  supxrunb1  11523  supxrunb2  11524  supxrbnd  11532  ixxub  11562  ixxlb  11563  elioc2  11599  elico2  11600  elicc2  11601  difreicc  11664  elfznelfzo  11895  flflp1  11924  modid  12000  modaddmodup  12030  modaddmodlo  12031  seqf1olem1  12126  facndiv  12346  faclbnd  12348  bcval5  12376  hashdom  12427  hashfacen  12483  seqcoll  12492  brfi1indlem  12511  brfi1uzind  12512  swrdn0  12634  swrdsymbeq  12651  revccat  12719  cshwsexa  12771  2cshwcshw  12772  cshwcsh2id  12775  seqshft  12897  sqrmo  13064  absmax  13141  rexico  13165  cau3lem  13166  limsupval2  13282  rlim2lt  13299  o1lo1  13339  rlimconst  13346  climrlim2  13349  2clim  13374  rlimcn2  13392  reccn2  13398  cn1lem  13399  o1of2  13414  lo1const  13422  climsqz  13442  climsqz2  13443  isercolllem2  13467  isercoll  13469  climsup  13471  climcau  13472  caucvgrlem2  13476  iseralt  13486  sumeq2ii  13494  fsum2dlem  13564  fsum0diag2  13577  cvgcmp  13609  cvgcmpce  13611  climcnds  13642  divrcnv  13643  mertenslem1  13672  mertens  13674  efaddlem  13706  tanaddlem  13778  sqrt2irr  13859  dvdseq  13908  dvdsext  13912  odd2np1  13921  bitsf1  13971  smuval2  14007  qredeq  14122  qredeu  14123  exprmfct  14126  isprm5  14128  rpexp1i  14137  nonsq  14167  powm2modprm  14203  iserodd  14234  pcz  14279  fldivp1  14291  pcfac  14293  expnprm  14296  prmpwdvds  14297  prmreclem5  14313  vdwapf  14365  vdwnnlem2  14389  0ramcl  14416  cshwsidrepswmod0  14453  cshwshashlem1  14454  cshwshash  14463  setscom  14536  firest  14704  isacs2  14924  mreacs  14929  acsfn  14930  acsfn1  14932  ressffth  15181  setcmon  15288  uncfcurf  15382  drsdirfi  15441  resmhm  15861  resmhm2  15862  mhmco  15864  pwsdiagmhm  15871  gsumwsubmcl  15877  gsumwmhm  15884  gsumwspan  15885  isgrpinv  15971  mulgz  16034  grpissubg  16092  resghm  16154  cntzsubm  16244  cntzmhm  16247  gsmsymgreqlem2  16327  symgfixf1  16333  f1omvdconj  16342  f1otrspeq  16343  f1omvdco2  16344  symggen  16366  odf1  16455  gexdvds  16475  pgpfi  16496  sylow3lem6  16523  lsmub1x  16537  lsmless12  16552  efgred2  16642  efgcpbllemb  16644  torsubg  16731  prmcyg  16767  ghmcyg  16769  gsumval3OLD  16779  telgsums  16893  dprdfadd  16930  dprdfaddOLD  16937  subgdmdprd  16951  dprdsn  16953  dmdprdsplitlem  16954  dmdprdsplitlemOLD  16955  dmdprdsplit2lem  16964  ablfacrp  16987  ablfac1b  16991  ablfac2  17010  mgpress  17022  irredrmul  17226  isdrng2  17275  drngmul0or  17286  issubdrg  17323  islss3  17474  lmhmco  17558  lmhmplusg  17559  pwsdiaglmhm  17572  lvecvs0or  17623  lbsextlem2  17674  2idlcpbl  17750  issubassa2  17862  evlslem3  18051  evlseu  18053  evlsval  18056  coe1tmmul2  18185  coe1tmmul  18186  qsssubdrg  18345  prmirredlem  18390  prmirredlemOLD  18393  mulgrhm2  18400  mulgrhm2OLD  18403  znidomb  18467  znunit  18469  cyggic  18478  evpmodpmf1o  18499  psgndiflemA  18504  pjfo  18613  obslbs  18628  uvcff  18689  lindfmm  18729  islinds4  18737  matassa  18813  mat1dimscm  18844  mat1dimcrng  18846  mat1mhm  18853  dmatmul  18866  1marepvmarrepid  18944  mdetleib2  18957  madutpos  19011  matunit  19047  cramer0  19059  mat2pmatghm  19098  mat2pmatmul  19099  mat2pmat1  19100  mat2pmatlin  19103  mat2pmatscmxcl  19108  monmatcollpw  19147  pmatcollpw3fi1lem1  19154  pmatcollpwscmatlem1  19157  pm2mpf1  19167  mp2pm2mplem4  19177  pm2mpghm  19184  chpscmat  19210  chpscmatgsumbin  19212  chfacffsupp  19224  chfacfscmul0  19226  chfacfscmulfsupp  19227  chfacfscmulgsum  19228  chfacfpmmul0  19230  chfacfpmmulfsupp  19231  chfacfpmmulgsum  19232  cayhamlem4  19256  tgdom  19346  fctop  19371  pptbas  19375  elcls3  19450  toponmre  19460  neiptopuni  19497  neiptoptop  19498  neiptopreu  19500  maxlp  19514  ssrest  19543  cnfval  19600  cnpfval  19601  iscnp3  19611  subbascn  19621  ssidcn  19622  cnpnei  19631  cncls2  19640  cncls  19641  cnntr  19642  cncnp  19647  restcnrm  19729  cmpsublem  19765  cmpsub  19766  cmpcld  19768  uncmp  19769  hauscmplem  19772  cmpfi  19774  iunconlem  19794  2ndcrest  19821  2ndcctbss  19822  2ndcomap  19825  2ndcsep  19826  1stcelcls  19828  lly1stc  19863  lfinpfin  19891  lfinun  19892  dissnref  19895  1stckgenlem  19920  ptval  19937  ptbasfi  19948  txcls  19971  tx1cn  19976  ptclsg  19982  xkoccn  19986  upxp  19990  xkococnlem  20026  imasnopn  20057  imasncld  20058  imasncls  20059  tgqtop  20079  qtopcld  20080  reghmph  20160  ptcmpfi  20180  filcon  20250  fbasrn  20251  filuni  20252  isufil2  20275  ssufl  20285  ufileu  20286  filufint  20287  ufilen  20297  rnelfm  20320  flimopn  20342  flimclsi  20345  hauspwpwf1  20354  isfcls  20376  fcfval  20400  alexsublem  20410  alexsubALTlem2  20414  alexsubALTlem3  20415  alexsubALTlem4  20416  ptcmplem2  20419  ptcmplem3  20420  cnextfval  20428  symgtgp  20466  opnsubg  20472  clsnsg  20474  tsmsresOLD  20511  tsmsres  20512  tsmsf1o  20513  restutopopn  20607  neipcfilu  20665  stdbdmet  20885  metcnp  20910  metustidOLD  20928  metustid  20929  metustsymOLD  20930  metustsym  20931  metustblOLD  20949  metustbl  20950  metutopOLD  20951  psmetutop  20952  isngp2  20983  subgngp  21015  ngptgp  21016  tngtopn  21030  sranlm  21059  nlmvscn  21062  nmo0  21108  nmoco  21110  qdensere  21143  iocopnst  21306  oprpiece1res2  21318  evth2  21326  xlebnum  21331  lebnumii  21332  pcoass  21390  nmoleub2lem3  21464  nmhmcn  21469  lmnn  21568  cfilfcls  21579  iscmet3lem1  21596  iscmet3lem2  21597  causs  21603  equivcfil  21604  lmclim  21607  lmcau  21617  flimcfil  21618  cmetss  21619  relcmpcmet  21621  bcthlem4  21632  bcthlem5  21633  minveclem3  21710  ovoliunlem2  21780  ovolicc2lem4  21797  nulmbl2  21813  iundisj  21824  ioombl1lem4  21837  vitalilem1  21883  vitali  21888  mbfconstlem  21902  mbfimaicc  21906  mbfimaopnlem  21928  mbfsup  21937  i1fd  21954  i1fmullem  21967  i1fadd  21968  itg1addlem4  21972  itg1addlem5  21973  i1fres  21978  itg10a  21983  itg1climres  21987  mbfi1fseqlem3  21990  mbfi1fseqlem4  21991  mbfi1fseqlem5  21992  itg2const2  22014  itg2seq  22015  itg2monolem1  22023  itg2mono  22026  itg2i1fseqle  22027  itg2cnlem1  22034  iblitg  22041  ibl0  22059  itgss  22084  itgeqa  22086  iblabsr  22102  iblmulc2  22103  bddmulibl  22111  dvnff  22192  dvcobr  22215  dvrec  22224  dvmptfsum  22242  dvexp3  22245  c1liplem1  22263  c1lip1  22264  dvgt0lem1  22269  tdeglem4  22324  ply1divex  22403  q1pval  22420  fta1g  22434  plyco0  22455  plyeq0lem  22473  plymullem1  22477  plyco  22504  coemullem  22512  coemulhi  22516  coemulc  22517  coe1termlem  22520  dgrlt  22528  dgrco  22537  plycjlem  22538  dvply1  22545  plydivex  22558  fta1  22569  aalioulem2  22594  aalioulem3  22595  aalioulem6  22598  aaliou  22599  taylfval  22619  ulmcaulem  22654  ulmcau  22655  itgulm  22668  pserdvlem2  22688  pilem2  22712  divlogrlim  22880  logcnlem5  22891  advlogexp  22900  cxpcn3  22986  atantayl2  23133  leibpi  23137  birthdaylem3  23147  rlimcnp  23159  cxplim  23165  cxploglim2  23172  ftalem3  23212  basellem2  23219  mumullem1  23317  sqff1o  23320  muinv  23333  chtublem  23350  vmasum  23355  logfac2  23356  mersenne  23366  dchrptlem1  23403  bposlem1  23423  bposlem3  23425  bposlem5  23427  lgslem4  23438  lgsval2lem  23445  lgsmod  23460  lgsdir2lem4  23465  lgsdinn0  23479  lgsquad2lem2  23498  lgsquad3  23500  2sqlem6  23508  2sqlem7  23509  dchrisumlem3  23540  dchrmusumlema  23542  dchrmusum2  23543  dchrvmasumlem1  23544  dchrvmasum2lem  23545  dchrvmasumlem2  23547  dchrvmasumiflem1  23550  dchrisum0lema  23563  dchrisum0lem2a  23566  dchrisum0lem2  23567  mulog2sumlem2  23584  selberg  23597  pntsval2  23625  pntibnd  23642  pntlem3  23658  ostthlem1  23676  ostth2lem2  23683  ostth3  23687  brbtwn2  24040  colinearalglem4  24044  colinearalg  24045  axsegconlem8  24059  axsegconlem9  24060  axsegconlem10  24061  ax5seglem3  24066  ax5seglem5  24068  axbtwnid  24074  axlowdimlem17  24093  axeuclid  24098  axcontlem2  24100  axcontlem7  24105  axcontlem8  24106  usgrares1  24242  nbgraf1olem1  24273  nb3graprlem1  24283  cusgrasize2inds  24309  cusgrafilem2  24312  2wlklem1  24431  constr2wlk  24432  usgra2wlkspthlem1  24451  constr3trl  24491  constr3pth  24492  constr3cycl  24493  wwlkn0s  24537  wwlknext  24556  wwlknextbi  24557  wwlkextfun  24561  wwlkextproplem3  24575  clwwlkn2  24607  clwlkisclwwlklem2a4  24616  clwwlkf1  24628  wwlkext2clwwlk  24635  clwwisshclwwlem  24638  erclwwlkeqlen  24644  erclwwlksym  24646  erclwwlktr  24647  erclwwlkneqlen  24656  eleclclwwlkn  24665  hashecclwwlkn1  24666  usghashecclwwlk  24667  clwlkfclwwlk  24676  clwlkf1clwwlk  24682  el2spthonot0  24703  usgravd0nedg  24750  cusgraisrusgra  24770  rusgranumwlklem0  24780  rusgranumwlks  24788  iseupa  24797  eupath2  24812  frgra2v  24831  2pthfrgra  24843  frgrancvvdeqlem3  24864  frgrancvvdeqlemC  24871  frgrancvvdeqlem9  24873  frg2woteu  24887  frg2woteq  24892  extwwlkfablem2  24910  numclwwlkovf2ex  24918  numclwwlk1  24930  numclwwlk2lem1  24934  frgrareg  24949  grpoidinv  25041  grpoideu  25042  nvmul0or  25378  vacn  25435  smcnlem  25438  nmoub3i  25519  nmoo0  25537  blocnilem  25550  ubthlem1  25617  ubthlem2  25618  ubthlem3  25619  minvecolem3  25623  hvmul0or  25773  hvmulcan  25820  hvaddsub4  25826  his35  25836  occon  26036  ocorth  26040  occl  26053  chscllem2  26387  5oalem1  26403  5oalem2  26404  3oalem2  26412  pjds3i  26462  nmopub2tALT  26659  nmfnleub2  26676  hmopadj2  26691  0cnop  26729  0cnfn  26730  nmophmi  26781  cnlnadjlem6  26822  leopnmid  26888  nmopleid  26889  opsqrlem1  26890  pjss2coi  26914  pjssdif1i  26925  pj3cor1i  26959  mdsl0  27060  mdslmd1lem1  27075  mdslmd1lem2  27076  csmdsymi  27084  superpos  27104  atomli  27132  chirredlem2  27141  chirredlem3  27142  atcvat3i  27146  atcvat4i  27147  mdsymlem5  27157  cdjreui  27182  cdj1i  27183  foresf1o  27234  rabfodom  27235  disjdifprg  27267  iundisjf  27279  fcnvgreu  27345  fpwrelmap  27387  xaddeq0  27404  iundisjfi  27432  ishashinf  27437  xrsmulgzz  27498  xrge0adddir  27514  abliso  27518  submomnd  27532  ofldchr  27636  suborng  27637  locfinreflem  27675  pcmplfinf  27696  xrge0iifiso  27749  pnfneige0  27765  lmxrge0  27766  gsumesum  27899  esumlub  27900  esumcst  27903  insiga  27969  measinb  28024  cntmeas  28029  imambfm  28065  eulerpartlemgvv  28147  rrvsum  28225  ballotlemsv  28280  ballotlemsima  28286  plymulx0  28336  signsplypnf  28339  signsply0  28340  signswmnd  28346  derangenlem  28447  subfacp1lem6  28461  conpcon  28512  txscon  28518  mrsubrn  28705  msubco  28723  ntrivcvg  28965  prodeq2ii  28979  fprod2dlem  29044  fundmpss  29130  dftrpred3g  29250  poseq  29267  soseq  29268  sltval2  29350  nobndlem6  29391  fin2so  29974  mblfinlem2  29986  mblfinlem3  29987  ismblfin  29989  cnambfre  29997  itg2addnclem  30000  itg2addnclem2  30001  itg2addnclem3  30002  itg2addnc  30003  itg2gt0cn  30004  iblabsnclem  30012  iblmulc2nc  30014  ftc1cnnc  30023  ftc1anclem5  30028  ftc1anclem6  30029  ftc1anclem7  30030  ftc1anclem8  30031  ftc1anc  30032  finminlem  30070  nn0prpwlem  30074  neibastop3  30114  fgmin  30122  filbcmb  30165  sdclem1  30170  fdc  30172  nnubfi  30177  nninfnub  30178  geomcau  30186  istotbnd3  30201  sstotbnd3  30206  isbnd3  30214  ssbnd  30218  prdsbnd  30223  cntotbnd  30226  heiborlem8  30248  bfplem2  30253  rrncmslem  30262  rngoisocnv  30318  unichnidl  30362  keridl  30363  prnc  30398  elrfirn  30561  isnacs3  30576  mzpsubmpt  30609  mzprename  30616  lzunuz  30635  eldiophss  30642  eqrabdioph  30645  rexrabdioph  30661  rabdiophlem2  30669  ctbnfien  30686  irrapxlem1  30692  irrapxlem2  30693  irrapxlem4  30695  pell1234qrreccl  30724  pell1234qrmulcl  30725  pell14qrgt0  30729  pell1234qrdich  30731  pell1qrgaplem  30743  pellqrex  30749  reglogltb  30761  reglogleb  30762  monotoddzzfi  30812  oddcomabszz  30814  jm2.24  30835  congsym  30840  acongtr  30850  acongrep  30852  jm2.18  30864  jm2.23  30872  jm2.26a  30876  jm2.26lem3  30877  jm2.27b  30882  rmydioph  30890  setindtr  30900  wepwsolem  30921  dnnumch1  30924  fnwe2lem2  30931  aomclem6  30939  dfac21  30946  islssfg  30950  lnmlsslnm  30961  pwslnm  30974  lnrfg  31002  dgrsub2  31018  mpaaeu  31034  rngunsnply  31057  acsfn1p  31083  cntzsdrg  31086  idomodle  31088  prmunb2  31124  isprm7  31125  dvdslcm  31134  lcmneg  31139  lcmgcdlem  31142  fmuldfeqlem1  31461  fmuldfeq  31462  climrec  31474  climinf  31477  climsuse  31479  limciccioolb  31492  constlimc  31495  limcrecl  31500  sumnnodd  31501  lptioo2  31502  lptioo1  31503  limcicciooub  31508  islpcn  31510  limsupre  31512  limcresiooub  31513  limcresioolb  31514  0ellimcdiv  31520  icccncfext  31555  fperdvper  31577  dvbdfbdioolem2  31588  ioodvbdlimc1lem1  31590  itgsinexp  31601  iblsplit  31613  iblspltprt  31620  itgioocnicc  31624  iblcncfioo  31625  itgspltprt  31626  stoweidlem3  31632  stoweidlem7  31636  stoweidlem14  31643  stoweidlem29  31658  stoweidlem34  31663  stoweidlem44  31673  stoweidlem46  31675  dirkerper  31725  dirkertrigeq  31730  dirkeritg  31731  dirkercncflem1  31732  dirkercncflem2  31733  dirkercncf  31736  fourierdlem12  31748  fourierdlem15  31751  fourierdlem17  31753  fourierdlem34  31770  fourierdlem35  31771  fourierdlem41  31777  fourierdlem42  31778  fourierdlem43  31779  fourierdlem46  31782  fourierdlem47  31783  fourierdlem48  31784  fourierdlem49  31785  fourierdlem50  31786  fourierdlem51  31787  fourierdlem63  31799  fourierdlem64  31800  fourierdlem65  31801  fourierdlem66  31802  fourierdlem71  31807  fourierdlem72  31808  fourierdlem73  31809  fourierdlem79  31815  fourierdlem81  31817  fourierdlem82  31818  fourierdlem83  31819  fourierdlem87  31823  fourierdlem97  31833  fourierdlem101  31837  fourierdlem102  31838  fourierdlem103  31839  fourierdlem104  31840  fourierdlem111  31847  fourierdlem114  31850  fourierswlem  31860  fouriersw  31861  2reu4a  31990  funressnfv  32009  f1dmvrnfibi  32108  usgra2pthlem1  32149  isrng  32322  uzlidlring  32335  ringcinv  32378  funcringcsetclem9  32390  lcosslsp  32526  ldepspr  32561  bnj1098  33327  bnj1118  33525  bnj1417  33582  cvrval5  34617  3dim0  34659  pmapglbx  34971  pclfinclN  35152  lhplt  35202  lhpexle1  35210  lhpocnle  35218  lhpjat1  35222  lhpjat2  35223  lhpj1  35224  lhpmcvr  35225  lhpmcvr2  35226  lhpm0atN  35231  lhpmat  35232  ltrnid  35337  trlcl  35366  trlle  35386  cdlemc4  35396  cdleme0cp  35416  cdleme0cq  35417  cdlemeulpq  35422  cdleme1b  35428  cdleme1  35429  cdleme2  35430  cdleme3b  35431  cdleme3c  35432  cdlemedb  35499  cdleme27a  35569  docaclN  36327  doca2N  36329  djajN  36340  dihglblem5apreN  36494
  Copyright terms: Public domain W3C validator