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  755  simplrl  761  simplrr  762  ax12eq  2272  ax12el  2273  frsn  5079  sofld  5461  foun  5840  f1oprg  5862  fvreseq1  5989  foeqcnvco  6204  f1eqcocnv  6205  caovord3  6487  tfindsg  6694  soex  6742  curry1  6891  curry2  6894  f1o2ndf1  6907  suppfnss  6943  mpt2xopxnop0  6961  smores2  7043  smo11  7053  smoord  7054  oesuclem  7193  oelim  7202  oaordi  7213  oaass  7228  odi  7246  omass  7247  oen0  7253  oelim2  7262  nnaordi  7285  eceqoveq  7434  resixpfo  7526  boxcutc  7531  xpdom2  7631  domunsncan  7636  omxpenlem  7637  mapen  7700  xpmapenlem  7703  mapdom2  7707  php3  7722  onomeneq  7726  fineqvlem  7753  xpfi  7809  fiint  7815  dffi3  7909  marypha1lem  7911  ordtypelem7  7967  wemaplem3  7991  brwdom2  8017  unxpwdom2  8032  cantnfle  8107  cantnflt  8108  cantnfleOLD  8137  cantnfltOLD  8138  r1pwss  8219  rankval3b  8261  carddomi2  8368  isinffi  8390  fidomtri  8391  acndom  8449  dfac9  8533  dfac12lem1  8540  dfac12lem2  8541  ackbij1lem16  8632  ackbij2lem3  8638  fictb  8642  cofsmo  8666  cfsmolem  8667  cfcof  8671  infpssrlem4  8703  fin23lem39  8747  isf32lem2  8751  isf32lem3  8752  fin1a2lem12  8808  fin1a2lem13  8809  fin12  8810  axdc3lem4  8850  axdc4lem  8852  ttukeylem3  8908  carden  8943  axrepnd  8986  canthwelem  9045  inawinalem  9084  gchina  9094  r1limwun  9131  inar1  9170  inatsk  9173  tskuni  9178  intgru  9209  nqereu  9324  ltexnq  9370  npex  9381  elnp  9382  prlem936  9442  recexsrlem  9497  mul02lem1  9773  lemul12a  10421  mulge0b  10433  lediv12a  10458  lediv2a  10459  creur  10550  peano5nni  10559  nndiv  10597  rpnnen1lem1  11233  rpnnen1lem2  11234  rpnnen1lem3  11235  rpnnen1lem5  11237  xrmax2  11402  qextltlem  11426  xpncan  11468  xmulneg1  11486  xmulge0  11501  xlemul1a  11505  xrsupsslem  11523  xrinfmsslem  11524  xrub  11528  supxrun  11532  supxrunb1  11536  supxrunb2  11537  supxrbnd  11545  ixxub  11575  ixxlb  11576  elioc2  11612  elico2  11613  elicc2  11614  difreicc  11677  elfznelfzo  11917  flflp1  11946  modid  12022  modaddmodup  12052  modaddmodlo  12053  seqf1olem1  12148  facndiv  12368  faclbnd  12370  bcval5  12398  hashdom  12449  hashfacen  12506  seqcoll  12515  brfi1indlem  12534  brfi1uzind  12535  ccatw2s1p2  12649  swrdsymbeq  12680  revccat  12751  cshwsexa  12803  2cshwcshw  12804  cshwcsh2id  12807  seqshft  12929  sqrmo  13096  absmax  13173  rexico  13197  cau3lem  13198  limsupval2  13314  rlim2lt  13331  o1lo1  13371  rlimconst  13378  climrlim2  13381  2clim  13406  rlimcn2  13424  reccn2  13430  cn1lem  13431  o1of2  13446  lo1const  13454  climsqz  13474  climsqz2  13475  isercolllem2  13499  isercoll  13501  climsup  13503  climcau  13504  caucvgrlem2  13508  iseralt  13518  sumeq2ii  13526  fsum2dlem  13596  fsum0diag2  13609  cvgcmp  13641  cvgcmpce  13643  climcnds  13674  divrcnv  13675  mertenslem1  13704  mertens  13706  ntrivcvg  13717  prodeq2ii  13731  fprod2dlem  13795  efaddlem  13839  tanaddlem  13912  sqrt2irr  13993  dvdseq  14044  dvdsext  14048  odd2np1  14057  bitsf1  14107  smuval2  14143  qredeq  14258  qredeu  14259  exprmfct  14262  isprm5  14264  rpexp1i  14273  nonsq  14303  powm2modprm  14339  iserodd  14370  pcz  14415  fldivp1  14427  pcfac  14429  expnprm  14432  prmpwdvds  14433  prmreclem5  14449  vdwapf  14501  vdwnnlem2  14525  0ramcl  14552  cshwsidrepswmod0  14590  cshwshashlem1  14591  cshwshash  14600  setscom  14675  firest  14849  isacs2  15069  mreacs  15074  acsfn  15075  acsfn1  15077  ressffth  15353  setcmon  15492  funcestrcsetclem9  15543  funcsetcestrclem9  15558  uncfcurf  15634  drsdirfi  15693  resmhm  16116  resmhm2  16117  mhmco  16119  pwsdiagmhm  16126  gsumwsubmcl  16132  gsumwmhm  16139  gsumwspan  16140  isgrpinv  16226  mulgz  16289  grpissubg  16347  resghm  16409  cntzsubm  16499  cntzmhm  16502  gsmsymgreqlem2  16582  symgfixf1  16588  f1omvdconj  16597  f1otrspeq  16598  f1omvdco2  16599  symggen  16621  odf1  16710  gexdvds  16730  pgpfi  16751  sylow3lem6  16778  lsmub1x  16792  lsmless12  16807  efgred2  16897  efgcpbllemb  16899  torsubg  16986  prmcyg  17022  ghmcyg  17024  gsumval3OLD  17034  telgsums  17148  dprdfadd  17186  dprdfaddOLD  17193  subgdmdprd  17207  dprdsn  17209  dmdprdsplitlem  17210  dmdprdsplitlemOLD  17211  dmdprdsplit2lem  17220  ablfacrp  17243  ablfac1b  17247  ablfac2  17266  mgpress  17278  irredrmul  17482  isdrng2  17532  drngmul0or  17543  issubdrg  17580  islss3  17731  lmhmco  17815  lmhmplusg  17816  pwsdiaglmhm  17829  lvecvs0or  17880  lbsextlem2  17931  2idlcpbl  18008  issubassa2  18120  evlslem3  18309  evlseu  18311  evlsval  18314  coe1tmmul2  18443  coe1tmmul  18444  qsssubdrg  18603  prmirredlem  18649  prmirredlemOLD  18652  mulgrhm2  18659  mulgrhm2OLD  18662  znidomb  18726  znunit  18728  cyggic  18737  evpmodpmf1o  18758  psgndiflemA  18763  pjfo  18872  obslbs  18887  uvcff  18948  lindfmm  18988  islinds4  18996  matassa  19072  mat1dimscm  19103  mat1dimcrng  19105  mat1mhm  19112  dmatmul  19125  1marepvmarrepid  19203  mdetleib2  19216  madutpos  19270  matunit  19306  cramer0  19318  mat2pmatghm  19357  mat2pmatmul  19358  mat2pmat1  19359  mat2pmatlin  19362  mat2pmatscmxcl  19367  monmatcollpw  19406  pmatcollpw3fi1lem1  19413  pmatcollpwscmatlem1  19416  pm2mpf1  19426  mp2pm2mplem4  19436  pm2mpghm  19443  chpscmat  19469  chpscmatgsumbin  19471  chfacffsupp  19483  chfacfscmul0  19485  chfacfscmulfsupp  19486  chfacfscmulgsum  19487  chfacfpmmul0  19489  chfacfpmmulfsupp  19490  chfacfpmmulgsum  19491  cayhamlem4  19515  tgdom  19606  fctop  19631  pptbas  19635  elcls3  19710  toponmre  19720  neiptopuni  19757  neiptoptop  19758  neiptopreu  19760  maxlp  19774  ssrest  19803  cnfval  19860  cnpfval  19861  iscnp3  19871  subbascn  19881  ssidcn  19882  cnpnei  19891  cncls2  19900  cncls  19901  cnntr  19902  cncnp  19907  restcnrm  19989  cmpsublem  20025  cmpsub  20026  cmpcld  20028  uncmp  20029  hauscmplem  20032  cmpfi  20034  iunconlem  20053  2ndcrest  20080  2ndcctbss  20081  2ndcomap  20084  2ndcsep  20085  1stcelcls  20087  lly1stc  20122  lfinpfin  20150  lfinun  20151  dissnref  20154  1stckgenlem  20179  ptval  20196  ptbasfi  20207  txcls  20230  tx1cn  20235  ptclsg  20241  xkoccn  20245  upxp  20249  xkococnlem  20285  imasnopn  20316  imasncld  20317  imasncls  20318  tgqtop  20338  qtopcld  20339  reghmph  20419  ptcmpfi  20439  filcon  20509  fbasrn  20510  filuni  20511  isufil2  20534  ssufl  20544  ufileu  20545  filufint  20546  ufilen  20556  rnelfm  20579  flimopn  20601  flimclsi  20604  hauspwpwf1  20613  isfcls  20635  fcfval  20659  alexsublem  20669  alexsubALTlem2  20673  alexsubALTlem3  20674  alexsubALTlem4  20675  ptcmplem2  20678  ptcmplem3  20679  cnextfval  20687  symgtgp  20725  opnsubg  20731  clsnsg  20733  tsmsresOLD  20770  tsmsres  20771  tsmsf1o  20772  restutopopn  20866  neipcfilu  20924  stdbdmet  21144  metcnp  21169  metustidOLD  21187  metustid  21188  metustsymOLD  21189  metustsym  21190  metustblOLD  21208  metustbl  21209  metutopOLD  21210  psmetutop  21211  isngp2  21242  subgngp  21274  ngptgp  21275  tngtopn  21289  sranlm  21318  nlmvscn  21321  nmo0  21367  nmoco  21369  qdensere  21402  iocopnst  21565  oprpiece1res2  21577  evth2  21585  xlebnum  21590  lebnumii  21591  pcoass  21649  nmoleub2lem3  21723  nmhmcn  21728  lmnn  21827  cfilfcls  21838  iscmet3lem1  21855  iscmet3lem2  21856  causs  21862  equivcfil  21863  lmclim  21866  lmcau  21876  flimcfil  21877  cmetss  21878  relcmpcmet  21880  bcthlem4  21891  bcthlem5  21892  minveclem3  21969  ovoliunlem2  22039  ovolicc2lem4  22056  nulmbl2  22072  iundisj  22083  ioombl1lem4  22096  vitalilem1  22142  vitali  22147  mbfconstlem  22161  mbfimaicc  22165  mbfimaopnlem  22187  mbfsup  22196  i1fd  22213  i1fmullem  22226  i1fadd  22227  itg1addlem4  22231  itg1addlem5  22232  i1fres  22237  itg10a  22242  itg1climres  22246  mbfi1fseqlem3  22249  mbfi1fseqlem4  22250  mbfi1fseqlem5  22251  itg2const2  22273  itg2seq  22274  itg2monolem1  22282  itg2mono  22285  itg2i1fseqle  22286  itg2cnlem1  22293  iblitg  22300  ibl0  22318  itgss  22343  itgeqa  22345  iblabsr  22361  iblmulc2  22362  bddmulibl  22370  dvnff  22451  dvcobr  22474  dvrec  22483  dvmptfsum  22501  dvexp3  22504  c1liplem1  22522  c1lip1  22523  dvgt0lem1  22528  tdeglem4  22583  ply1divex  22662  q1pval  22679  fta1g  22693  plyco0  22714  plyeq0lem  22732  plymullem1  22736  plyco  22763  coemullem  22772  coemulhi  22776  coemulc  22777  coe1termlem  22780  dgrlt  22788  dgrco  22797  plycjlem  22798  dvply1  22805  plydivex  22818  fta1  22829  aalioulem2  22854  aalioulem3  22855  aalioulem6  22858  aaliou  22859  taylfval  22879  ulmcaulem  22914  ulmcau  22915  itgulm  22928  pserdvlem2  22948  pilem2  22972  divlogrlim  23141  logcnlem5  23152  advlogexp  23161  cxpcn3  23247  atantayl2  23394  leibpi  23398  birthdaylem3  23408  rlimcnp  23420  cxplim  23426  cxploglim2  23433  ftalem3  23473  basellem2  23480  mumullem1  23578  sqff1o  23581  muinv  23594  chtublem  23611  vmasum  23616  logfac2  23617  mersenne  23627  dchrptlem1  23664  bposlem1  23684  bposlem3  23686  bposlem5  23688  lgslem4  23699  lgsval2lem  23706  lgsmod  23721  lgsdir2lem4  23726  lgsdinn0  23740  lgsquad2lem2  23759  lgsquad3  23761  2sqlem6  23769  2sqlem7  23770  dchrisumlem3  23801  dchrmusumlema  23803  dchrmusum2  23804  dchrvmasumlem1  23805  dchrvmasum2lem  23806  dchrvmasumlem2  23808  dchrvmasumiflem1  23811  dchrisum0lema  23824  dchrisum0lem2a  23827  dchrisum0lem2  23828  mulog2sumlem2  23845  selberg  23858  pntsval2  23886  pntibnd  23903  pntlem3  23919  ostthlem1  23937  ostth2lem2  23944  ostth3  23948  brbtwn2  24334  colinearalglem4  24338  colinearalg  24339  axsegconlem8  24353  axsegconlem9  24354  axsegconlem10  24355  ax5seglem3  24360  ax5seglem5  24362  axbtwnid  24368  axlowdimlem17  24387  axeuclid  24392  axcontlem2  24394  axcontlem7  24399  axcontlem8  24400  usgrares1  24536  nbgraf1olem1  24567  nb3graprlem1  24577  cusgrasize2inds  24603  cusgrafilem2  24606  2wlklem1  24725  constr2wlk  24726  usgra2wlkspthlem1  24745  constr3trl  24785  constr3pth  24786  constr3cycl  24787  wwlkn0s  24831  wwlknext  24850  wwlknextbi  24851  wwlkextfun  24855  wwlkextproplem3  24869  clwwlkn2  24901  clwlkisclwwlklem2a4  24910  clwwlkf1  24922  wwlkext2clwwlk  24929  clwwisshclwwlem  24932  erclwwlkeqlen  24938  erclwwlksym  24940  erclwwlktr  24941  erclwwlkneqlen  24950  eleclclwwlkn  24959  hashecclwwlkn1  24960  usghashecclwwlk  24961  clwlkfclwwlk  24970  clwlkf1clwwlk  24976  el2spthonot0  24997  usgravd0nedg  25044  cusgraisrusgra  25064  rusgranumwlklem0  25074  rusgranumwlks  25082  iseupa  25091  eupath2  25106  frgra2v  25125  2pthfrgra  25137  frgrancvvdeqlem3  25158  frgrancvvdeqlemC  25165  frgrancvvdeqlem9  25167  frg2woteu  25181  frg2woteq  25186  extwwlkfablem2  25204  numclwwlkovf2ex  25212  numclwwlk1  25224  numclwwlk2lem1  25228  frgrareg  25243  grpoidinv  25336  grpoideu  25337  nvmul0or  25673  vacn  25730  smcnlem  25733  nmoub3i  25814  nmoo0  25832  blocnilem  25845  ubthlem1  25912  ubthlem2  25913  ubthlem3  25914  minvecolem3  25918  hvmul0or  26068  hvmulcan  26115  hvaddsub4  26121  his35  26131  occon  26331  ocorth  26335  occl  26348  chscllem2  26682  5oalem1  26698  5oalem2  26699  3oalem2  26707  pjds3i  26757  nmopub2tALT  26954  nmfnleub2  26971  hmopadj2  26986  0cnop  27024  0cnfn  27025  nmophmi  27076  cnlnadjlem6  27117  leopnmid  27183  nmopleid  27184  opsqrlem1  27185  pjss2coi  27209  pjssdif1i  27220  pj3cor1i  27254  mdsl0  27355  mdslmd1lem1  27370  mdslmd1lem2  27371  csmdsymi  27379  superpos  27399  atomli  27427  chirredlem2  27436  chirredlem3  27437  atcvat3i  27441  atcvat4i  27442  mdsymlem5  27452  cdjreui  27477  cdj1i  27478  foresf1o  27530  rabfodom  27531  disjdifprg  27573  iundisjf  27585  fcnvgreu  27662  fpwrelmap  27706  xaddeq0  27723  iundisjfi  27753  ishashinf  27758  xrsmulgzz  27818  xrge0adddir  27834  abliso  27838  submomnd  27852  ofldchr  27957  suborng  27958  locfinreflem  27996  pcmplfinf  28017  xrge0iifiso  28070  pnfneige0  28086  lmxrge0  28087  gsumesum  28222  esumlub  28223  esumcst  28226  esum2dlem  28252  esum2d  28253  insiga  28298  measinb  28353  cntmeas  28358  imambfm  28394  omsf  28428  omssubadd  28432  eulerpartlemgvv  28490  rrvsum  28568  ballotlemsv  28623  ballotlemsima  28629  plymulx0  28679  signsplypnf  28682  signsply0  28683  signswmnd  28689  derangenlem  28790  subfacp1lem6  28804  conpcon  28855  txscon  28861  mrsubrn  29048  msubco  29066  fundmpss  29371  dftrpred3g  29490  poseq  29507  soseq  29508  sltval2  29590  nobndlem6  29631  fin2so  30202  mblfinlem2  30214  mblfinlem3  30215  ismblfin  30217  cnambfre  30225  itg2addnclem  30228  itg2addnclem2  30229  itg2addnclem3  30230  itg2addnc  30231  itg2gt0cn  30232  iblabsnclem  30240  iblmulc2nc  30242  ftc1cnnc  30251  ftc1anclem5  30256  ftc1anclem6  30257  ftc1anclem7  30258  ftc1anclem8  30259  ftc1anc  30260  finminlem  30298  nn0prpwlem  30302  neibastop3  30342  fgmin  30350  filbcmb  30393  sdclem1  30398  fdc  30400  nnubfi  30405  nninfnub  30406  geomcau  30414  istotbnd3  30429  sstotbnd3  30434  isbnd3  30442  ssbnd  30446  prdsbnd  30451  cntotbnd  30454  heiborlem8  30476  bfplem2  30481  rrncmslem  30490  rngoisocnv  30546  unichnidl  30590  keridl  30591  prnc  30626  elrfirn  30789  isnacs3  30804  mzpsubmpt  30837  mzprename  30844  lzunuz  30863  eldiophss  30870  eqrabdioph  30873  rexrabdioph  30889  rabdiophlem2  30897  ctbnfien  30914  irrapxlem1  30920  irrapxlem2  30921  irrapxlem4  30923  pell1234qrreccl  30952  pell1234qrmulcl  30953  pell14qrgt0  30957  pell1234qrdich  30959  pell1qrgaplem  30971  pellqrex  30977  reglogltb  30989  reglogleb  30990  monotoddzzfi  31040  oddcomabszz  31042  jm2.24  31063  congsym  31068  acongtr  31078  acongrep  31080  jm2.18  31092  jm2.23  31100  jm2.26a  31104  jm2.26lem3  31105  jm2.27b  31110  rmydioph  31118  setindtr  31128  wepwsolem  31149  dnnumch1  31152  fnwe2lem2  31159  aomclem6  31167  dfac21  31174  islssfg  31178  lnmlsslnm  31189  pwslnm  31202  lnrfg  31230  dgrsub2  31246  mpaaeu  31261  rngunsnply  31284  acsfn1p  31310  cntzsdrg  31313  idomodle  31315  prmunb2  31353  isprm7  31354  radcnvrat  31357  dvdslcm  31366  lcmneg  31371  lcmgcdlem  31374  binomcxplemfrat  31418  binomcxplemradcnv  31419  binomcxplemnotnn0  31423  fzdifsuc2  31673  fmuldfeqlem1  31737  fmuldfeq  31738  mccl  31767  climrec  31770  climinf  31773  climsuse  31775  limciccioolb  31788  constlimc  31791  limcrecl  31796  sumnnodd  31797  lptioo2  31798  lptioo1  31799  limcicciooub  31804  islpcn  31806  limsupre  31808  limcresiooub  31809  limcresioolb  31810  0ellimcdiv  31816  icccncfext  31851  fperdvper  31876  dvbdfbdioolem2  31887  dvnmptdivc  31896  dvnxpaek  31900  dvnmul  31901  dvmptfprod  31903  dvnprodlem1  31904  dvnprodlem2  31905  dvnprodlem3  31906  itgsinexp  31914  iblsplit  31926  iblspltprt  31933  itgioocnicc  31937  iblcncfioo  31938  itgspltprt  31939  stoweidlem3  31946  stoweidlem7  31950  stoweidlem14  31957  stoweidlem29  31972  stoweidlem34  31977  stoweidlem44  31987  stoweidlem46  31989  dirkerper  32039  dirkertrigeq  32044  dirkeritg  32045  dirkercncflem1  32046  dirkercncflem2  32047  dirkercncf  32050  fourierdlem12  32062  fourierdlem15  32065  fourierdlem17  32067  fourierdlem34  32084  fourierdlem35  32085  fourierdlem41  32091  fourierdlem42  32092  fourierdlem43  32093  fourierdlem46  32096  fourierdlem47  32097  fourierdlem48  32098  fourierdlem49  32099  fourierdlem50  32100  fourierdlem51  32101  fourierdlem63  32113  fourierdlem64  32114  fourierdlem65  32115  fourierdlem66  32116  fourierdlem71  32121  fourierdlem72  32122  fourierdlem73  32123  fourierdlem79  32129  fourierdlem81  32131  fourierdlem82  32132  fourierdlem83  32133  fourierdlem87  32137  fourierdlem97  32147  fourierdlem101  32151  fourierdlem102  32152  fourierdlem103  32153  fourierdlem104  32154  fourierdlem111  32161  fourierdlem114  32164  fourierswlem  32174  fouriersw  32175  elaa2lem  32177  elaa2  32178  etransclem17  32195  etransclem24  32202  etransclem25  32203  etransclem27  32205  etransclem32  32210  etransclem35  32213  2reu4a  32355  funressnfv  32374  pfxsymbeq  32480  f1dmvrnfibi  32534  usgra2pthlem1  32573  issubmgm2  32698  resmgmhm  32706  resmgmhm2  32707  mgmhmco  32709  isrng  32784  zrrnghm  32825  uzlidlring  32837  rngcinv  32891  rngcinvOLD  32903  ringcinv  32942  funcringcsetcOLD2lem9  32954  ringcinvOLD  32966  funcringcsetclem9OLD  32977  lcosslsp  33141  ldepspr  33176  bnj1098  33943  bnj1118  34141  bnj1417  34198  cvrval5  35240  3dim0  35282  pmapglbx  35594  pclfinclN  35775  lhplt  35825  lhpexle1  35833  lhpocnle  35841  lhpjat1  35845  lhpjat2  35846  lhpj1  35847  lhpmcvr  35848  lhpmcvr2  35849  lhpm0atN  35854  lhpmat  35855  ltrnid  35960  trlcl  35990  trlle  36010  cdlemc4  36020  cdleme0cp  36040  cdleme0cq  36041  cdlemeulpq  36046  cdleme1b  36052  cdleme1  36053  cdleme2  36054  cdleme3b  36055  cdleme3c  36056  cdlemedb  36123  cdleme27a  36194  docaclN  36952  doca2N  36954  djajN  36965  dihglblem5apreN  37119
  Copyright terms: Public domain W3C validator