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

Theorem ad2antlr 707
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 451 . 2  |-  ( (
ph  /\  th )  ->  ps )
32adantll 694 1  |-  ( ( ( ch  /\  ph )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ad3antlr  711  simplr  731  simplrl  736  simplrr  737  ax11eq  2145  ax11el  2146  tfindsg  4667  frsn  4776  sofld  5137  soex  5138  foun  5507  fcof1o  5819  foeqcnvco  5820  f1eqcocnv  5821  caovord3  6049  curry1  6226  curry2  6229  smores2  6387  smo11  6397  smoord  6398  oesuclem  6540  oelim  6549  oaordi  6560  oaass  6575  odi  6593  omass  6594  oen0  6600  oelim2  6609  nnaordi  6632  eceqoveq  6779  resixpfo  6870  boxcutc  6875  xpdom2  6973  domunsncan  6978  omxpenlem  6979  mapen  7041  xpmapenlem  7044  mapdom2  7048  php3  7063  onomeneq  7066  fineqvlem  7093  xpfi  7144  fiint  7149  dffi3  7200  marypha1lem  7202  ordtypelem7  7255  wemaplem3  7279  brwdom2  7303  unxpwdom2  7318  cantnfle  7388  cantnflt  7389  r1pwss  7472  rankval3b  7514  carddomi2  7619  isinffi  7641  fidomtri  7642  acndom  7694  dfac9  7778  dfac12lem1  7785  dfac12lem2  7786  infxp  7857  ackbij1lem16  7877  ackbij2lem3  7883  fictb  7887  cofsmo  7911  cfsmolem  7912  cfcof  7916  infpssrlem4  7948  fin23lem39  7992  isf32lem2  7996  isf32lem3  7997  fin1a2lem12  8053  fin1a2lem13  8054  fin12  8055  axdc3lem4  8095  axdc4lem  8097  ttukeylem3  8154  carden  8189  axrepnd  8232  canthwelem  8288  inawinalem  8327  gchina  8337  r1limwun  8374  inar1  8413  inatsk  8416  tskuni  8421  intgru  8452  nqereu  8569  ltexnq  8615  npex  8626  elnp  8627  prlem936  8687  recexsrlem  8741  mul02lem1  9004  lemul12a  9630  lediv12a  9665  lediv2a  9666  creur  9756  peano5nni  9765  nndiv  9802  rpnnen1lem1  10358  rpnnen1lem2  10359  rpnnen1lem3  10360  rpnnen1lem5  10362  xrmax2  10521  qextltlem  10545  xpncan  10587  xmulneg1  10605  xmulge0  10620  xlemul1a  10624  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  supxrun  10650  supxrunb1  10654  supxrunb2  10655  supxrbnd  10663  ixxub  10693  ixxlb  10694  elioc2  10729  elico2  10730  elicc2  10731  difreicc  10783  modid  11009  seqf1olem1  11101  facndiv  11317  faclbnd  11319  bcval5  11346  hashdom  11377  hashfacen  11408  seqcoll  11417  revccat  11500  seqshft  11596  sqrmo  11753  absmax  11829  rexico  11853  cau3lem  11854  limsupval2  11970  rlim2lt  11987  o1lo1  12027  rlimconst  12034  climrlim2  12037  2clim  12062  rlimcn2  12080  reccn2  12086  cn1lem  12087  o1of2  12102  lo1const  12110  climsqz  12130  climsqz2  12131  rlimsqzlem  12138  isercolllem2  12155  isercoll  12157  climsup  12159  climcau  12160  caucvgrlem2  12163  iseralt  12173  sumeq2ii  12182  fsum2dlem  12249  fsum0diag2  12261  cvgcmp  12290  cvgcmpce  12292  climcnds  12326  divrcnv  12327  mertenslem1  12356  mertens  12358  efaddlem  12390  tanaddlem  12462  sqr2irr  12543  dvdseq  12592  dvdsext  12595  odd2np1  12603  bitsf1  12653  smuval2  12689  qredeq  12801  qredeu  12802  exprmfct  12805  isprm5  12807  rpexp1i  12816  nonsq  12846  iserodd  12904  pcz  12949  fldivp1  12961  pcfac  12963  expnprm  12966  prmpwdvds  12967  prmreclem5  12983  vdwapf  13035  vdwnnlem2  13059  0ramcl  13086  setscom  13192  firest  13353  isacs2  13571  mreacs  13576  acsfn  13577  acsfn1  13579  ressffth  13828  setcmon  13935  uncfcurf  14029  drsdirfi  14088  lubid  14132  resmhm  14452  resmhm2  14453  mhmco  14455  pwsdiagmhm  14461  gsumwsubmcl  14477  gsumwmhm  14483  gsumwspan  14484  isgrpinv  14548  mulgz  14604  resghm  14715  cntzsubm  14827  cntzmhm  14830  odf1  14891  gexdvds  14911  pgpfi  14932  sylow3lem6  14959  lsmub1x  14973  lsmless12  14988  efgred2  15078  efgcpbllemb  15080  torsubg  15162  prmcyg  15196  ghmcyg  15198  gsumval3  15207  dprdfadd  15271  subgdmdprd  15285  dprdsn  15287  dmdprdsplitlem  15288  dmdprdsplit2lem  15296  ablfacrp  15317  ablfac1b  15321  ablfac2  15340  mgpress  15352  irredrmul  15505  isdrng2  15538  drngmul0or  15549  issubdrg  15586  islss3  15732  lmhmco  15816  lmhmplusg  15817  pwsdiaglmhm  15830  lvecvs0or  15877  lbsextlem2  15928  2idlcpbl  16002  issubassa2  16100  coe1tmmul2  16368  coe1tmmul  16369  qsssubdrg  16447  prmirredlem  16462  mulgrhm2  16477  znidomb  16531  znunit  16533  cyggic  16542  pjfo  16631  obslbs  16646  tgdom  16732  fctop  16757  pptbas  16761  elcls3  16836  toponmre  16846  maxlp  16894  restcld  16919  ssrest  16923  cnfval  16979  cnpfval  16980  iscnp3  16990  subbascn  17000  ssidcn  17001  cnpnei  17009  cncls2  17018  cncls  17019  cnntr  17020  cncnp  17025  restcnrm  17106  cmpsublem  17142  cmpsub  17143  cmpcld  17145  uncmp  17146  hauscmplem  17149  cmpfi  17151  iunconlem  17169  2ndcrest  17196  2ndcctbss  17197  2ndcomap  17200  2ndcsep  17201  1stcelcls  17203  lly1stc  17238  1stckgenlem  17264  ptval  17281  ptbasfi  17292  txcls  17315  tx1cn  17319  ptclsg  17325  xkoccn  17329  upxp  17333  txlly  17346  pthaus  17348  txhaus  17357  xkohaus  17363  xkococnlem  17369  tgqtop  17419  qtopcld  17420  reghmph  17500  ptcmpfi  17520  filcon  17594  fbasrn  17595  filuni  17596  isufil2  17619  ssufl  17629  ufileu  17630  filufint  17631  ufilen  17641  rnelfm  17664  flimopn  17686  flimclsi  17689  hauspwpwf1  17698  isfcls  17720  fcfval  17744  alexsublem  17754  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALTlem4  17760  ptcmplem2  17763  ptcmplem3  17764  symgtgp  17800  opnsubg  17806  clsnsg  17808  tsmsres  17842  tsmsf1o  17843  stdbdmet  18078  metcnp  18103  isngp2  18135  subgngp  18167  ngptgp  18168  tngtopn  18182  sranlm  18211  nlmvscn  18214  nmo0  18260  nmoco  18262  qdensere  18295  iocopnst  18454  oprpiece1res2  18466  evth2  18474  xlebnum  18479  lebnumii  18480  pcoass  18538  nmoleub2lem3  18612  nmhmcn  18617  lmnn  18705  cfilfcls  18716  iscmet3lem1  18733  iscmet3lem2  18734  causs  18740  equivcfil  18741  lmclim  18744  lmcau  18754  flimcfil  18755  cmetss  18756  relcmpcmet  18758  bcthlem4  18765  bcthlem5  18766  minveclem3  18809  ovoliunlem2  18878  ovolicc2lem4  18895  nulmbl2  18910  iundisj  18921  ioombl1lem4  18934  vitalilem1  18979  vitali  18984  mbfconstlem  19000  mbfimaicc  19004  mbfimaopnlem  19026  mbfsup  19035  i1fd  19052  i1fmullem  19065  i1fadd  19066  itg1addlem4  19070  itg1addlem5  19071  i1fres  19076  itg10a  19081  itg1climres  19085  mbfi1fseqlem3  19088  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  itg2const2  19112  itg2seq  19113  itg2monolem1  19121  itg2mono  19124  itg2i1fseqle  19125  itg2cnlem1  19132  iblitg  19139  ibl0  19157  itgss  19182  itgeqa  19184  iblabsr  19200  iblmulc2  19201  bddmulibl  19209  dvnff  19288  dvcobr  19311  dvrec  19320  dvmptfsum  19338  dvexp3  19341  c1liplem1  19359  c1lip1  19360  dvgt0lem1  19365  evlslem3  19414  evlseu  19416  evlsval  19419  tdeglem4  19462  ply1divex  19538  q1pval  19555  fta1g  19569  plyco0  19590  plyeq0lem  19608  plymullem1  19612  plyco  19639  coemullem  19647  coemulhi  19651  coemulc  19652  coe1termlem  19655  dgrlt  19663  dgrco  19672  plycjlem  19673  dvply1  19680  plydivex  19693  fta1  19704  aalioulem2  19729  aalioulem3  19730  aalioulem6  19733  aaliou  19734  taylfval  19754  ulmcaulem  19787  ulmcau  19788  itgulm  19800  pserdvlem2  19820  pilem2  19844  divlogrlim  19998  logcnlem5  20009  advlogexp  20018  cxpcn3  20104  atantayl2  20250  leibpi  20254  birthdaylem3  20264  rlimcnp  20276  cxplim  20282  cxploglim2  20289  ftalem3  20328  basellem2  20335  mumullem1  20433  sqff1o  20436  muinv  20449  chtublem  20466  vmasum  20471  logfac2  20472  mersenne  20482  dchrptlem1  20519  bposlem1  20539  bposlem3  20541  bposlem5  20543  lgslem4  20554  lgsval2lem  20561  lgsmod  20576  lgsdir2lem4  20581  lgsdinn0  20595  lgsquad2lem2  20614  lgsquad3  20616  2sqlem6  20624  2sqlem7  20625  dchrisumlem3  20656  dchrmusumlema  20658  dchrmusum2  20659  dchrvmasumlem1  20660  dchrvmasum2lem  20661  dchrvmasumlem2  20663  dchrvmasumiflem1  20666  dchrisum0lema  20679  dchrisum0lem2a  20682  dchrisum0lem2  20683  mulog2sumlem2  20700  selberg  20713  pntsval2  20741  pntibnd  20758  pntlem3  20774  ostthlem1  20792  ostth2lem2  20799  ostth3  20803  grpoidinv  20891  grpoideu  20892  nvmul0or  21226  vacn  21283  smcnlem  21286  nmoub3i  21367  nmoo0  21385  blocnilem  21398  ubthlem1  21465  ubthlem2  21466  ubthlem3  21467  minvecolem3  21471  hvmul0or  21620  hvmulcan  21667  hvaddsub4  21673  his35  21683  occon  21882  ocorth  21886  occl  21899  chscllem2  22233  5oalem1  22249  5oalem2  22250  3oalem2  22258  pjds3i  22308  nmopub2tALT  22505  nmfnleub2  22522  hmopadj2  22537  0cnop  22575  0cnfn  22576  nmophmi  22627  cnlnadjlem6  22668  leopnmid  22734  nmopleid  22735  opsqrlem1  22736  pjss2coi  22760  pjssdif1i  22771  pj3cor1i  22805  mdsl0  22906  mdslmd1lem1  22921  mdslmd1lem2  22922  csmdsymi  22930  superpos  22950  atomli  22978  chirredlem2  22987  chirredlem3  22988  atcvat3i  22992  atcvat4i  22993  mdsymlem5  23003  cdjreui  23028  cdj1i  23029  ballotlemsima  23090  xaddeq0  23319  xrsmulgzz  23322  xrge0adddir  23347  disjdifprg  23367  iundisjfi  23378  iundisjf  23380  pnfneige0  23389  lmxrge0  23390  ishashinf  23404  esumcst  23451  insiga  23513  measinb  23563  cntmeas  23568  imambfm  23582  derangenlem  23717  subfacp1lem6  23731  conpcon  23781  txscon  23787  iseupa  23896  eupath2  23919  mulge0b  24101  cprodeq2ii  24135  fundmpss  24193  dftrpred3g  24307  poseq  24324  soseq  24325  sltval2  24381  nobndlem6  24422  brbtwn2  24605  colinearalglem4  24609  colinearalg  24610  axsegconlem8  24624  axsegconlem9  24625  axsegconlem10  24626  ax5seglem3  24631  ax5seglem5  24633  axbtwnid  24639  axlowdimlem17  24658  axeuclid  24663  axcontlem2  24665  axcontlem7  24670  axcontlem8  24671  lxflflp1  25000  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  itg2gt0cn  25006  iblabsnclem  25014  iblmulc2nc  25016  ftc1cnnc  25025  mapmapmap  25251  prl2  25272  domrancur1c  25305  geme2  25378  muldisc  25584  osneisi  25634  prcnt  25654  cnpflf4  25667  limptlimpr2lem1  25677  altretop  25703  lvsovso  25729  cmpasso  25876  idsubfun  25961  pdiveql  26271  elicc3  26331  finminlem  26334  nn0prpwlem  26341  lfinpfin  26406  neibastop3  26414  fgmin  26422  filbcmb  26535  sdclem1  26556  fdc  26558  nnubfi  26563  nninfnub  26564  geomcau  26578  istotbnd3  26598  sstotbnd2  26601  sstotbnd3  26603  isbnd3  26611  ssbnd  26615  prdsbnd  26620  cntotbnd  26623  heiborlem8  26645  bfplem2  26650  rrncmslem  26659  rngoisocnv  26715  unichnidl  26759  keridl  26760  prnc  26795  elrfirn  26873  isnacs3  26888  mzpsubmpt  26924  mzprename  26930  lzunuz  26950  eldiophss  26957  eqrabdioph  26960  rexrabdioph  26978  rabdiophlem2  26986  ctbnfien  27004  irrapxlem1  27010  irrapxlem2  27011  irrapxlem4  27013  pell1234qrreccl  27042  pell1234qrmulcl  27043  pell14qrgt0  27047  pell1234qrdich  27049  pell1qrgaplem  27061  pellqrex  27067  reglogltb  27079  reglogleb  27080  monotoddzzfi  27130  oddcomabszz  27132  jm2.24  27153  congsym  27158  acongtr  27168  acongrep  27170  jm2.18  27184  jm2.23  27192  jm2.26a  27196  jm2.26lem3  27197  jm2.27b  27202  rmydioph  27210  setindtr  27220  wepwsolem  27241  dnnumch1  27244  fnwe2lem2  27251  aomclem6  27259  dfac21  27267  islssfg  27271  lnmlsslnm  27282  pwslnm  27299  uvcff  27343  lindfmm  27400  islinds4  27408  lnrfg  27426  dgrsub2  27442  mpaaeu  27458  rngunsnply  27481  f1omvdconj  27492  f1otrspeq  27493  f1omvdco2  27494  symggen  27514  matassa  27584  acsfn1p  27610  cntzsdrg  27613  idomodle  27615  fmuldfeqlem1  27815  fmuldfeq  27816  climrec  27832  climinf  27835  climsuse  27837  itgsinexp  27852  stoweidlem3  27855  stoweidlem7  27859  stoweidlem14  27866  stoweidlem29  27881  stoweidlem34  27886  stoweidlem46  27898  2reu4a  28070  funressnfv  28096  f1oprg  28186  mpt2xopxnop0  28197  elfznelfzo  28213  nb3graprlem1  28287  constr3trl  28405  constr3pth  28406  constr3cycl  28407  bnj1098  29131  bnj1118  29330  bnj1417  29387  cvrval5  30226  3dim0  30268  pmapglbx  30580  pclfinclN  30761  lhplt  30811  lhpexle1  30819  lhpocnle  30827  lhpjat1  30831  lhpjat2  30832  lhpj1  30833  lhpmcvr  30834  lhpmcvr2  30835  lhpm0atN  30840  lhpmat  30841  ltrnid  30946  trlcl  30975  trlle  30995  cdlemc4  31005  cdleme0cp  31025  cdleme0cq  31026  cdlemeulpq  31031  cdleme1b  31037  cdleme1  31038  cdleme2  31039  cdleme3b  31040  cdleme3c  31041  cdlemedb  31108  cdleme27a  31178  docaclN  31936  doca2N  31938  djajN  31949  dihglblem5apreN  32103
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 177  df-an 360
  Copyright terms: Public domain W3C validator