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

Theorem adantll 725
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Hypothesis
Ref Expression
adant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
adantll  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )

Proof of Theorem adantll
StepHypRef Expression
1 simpr 467 . 2  |-  ( ( th  /\  ph )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 478 1  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  ad2antlr  738  ad2ant2l  757  ad2ant2lr  759  3ad2antl3  1178  3adant1l  1268  ralcom2  2967  reu6  3239  sbc2iegf  3346  sbcralt  3352  pofun  4790  poinxp  4917  xpdifid  5284  sossfld  5302  predpo  5417  preddowncl  5426  tz7.7  5468  onfr  5481  ssimaex  5953  fndmdif  6009  dffo4  6061  foco2  6065  fcompt  6083  fconst2g  6143  isores3  6251  limsssuc  6704  curry1  6915  curry2  6918  extmptsuppeq  6966  suppss  6972  suppssov1  6974  suppss2  6976  suppssfv  6978  onnseq  7089  oe0  7250  oesuclem  7253  oecl  7265  oaordi  7273  oawordri  7277  oaass  7288  omordi  7293  omword2  7301  omlimcl  7305  odi  7306  omass  7307  oeoe  7326  nnaordi  7345  oaabs  7371  omsmolem  7380  eceqoveq  7494  dom2lem  7635  sbthlem9  7716  php3  7784  onomeneq  7788  isinf  7811  frfi  7842  fiint  7874  fodomfib  7877  fofinf1o  7878  marypha1lem  7973  ordiso2  8056  unwdomg  8125  xpwdomg  8126  ac5num  8493  cff1  8714  cfcoflem  8728  infpssrlem4  8762  isf32lem9  8817  isf34lem7  8835  fin1a2lem13  8868  fin1a2s  8870  hsmexlem4  8885  axdc2lem  8904  zorn2lem6  8957  axpowndlem2  9049  inttsk  9225  tskuni  9234  nqereu  9380  prcdnq  9444  addclprlem2  9468  ltexpri  9494  prlem936  9498  reclem2pr  9499  axsup  9735  add4  9875  ltleadd  10125  lt2mul2div  10511  lediv12a  10527  infmrclOLD  10621  nn2ge  10662  zextle  11038  fnn0ind  11063  xrlttr  11468  ifle  11519  xaddass  11564  xmulasslem3  11601  xlemul1a  11603  xadddilem  11609  xrsupsslem  11621  xrinfmsslem  11622  supxrunb1  11634  supxrunb2  11635  ixxin  11681  difreicc  11793  iccsplit  11794  iccshftr  11795  iccshftl  11797  iccdil  11799  icccntr  11801  fzaddel  11862  fzrev  11887  modadd1  12166  modmul1  12175  mulexp  12343  expadd  12346  expmul  12349  leexp1a  12363  expnbnd  12433  bccl  12539  hashdom  12590  prsshashgt1  12619  hashfacen  12650  brfi1uzind  12684  wrdnval  12733  swrdccat3blem  12888  revccat  12908  2shfti  13192  rexico  13465  cau3lem  13466  subcn2  13707  caucvgb  13795  iseraltlem1  13797  sumss  13839  incexclem  13943  supcvg  13963  mertenslem2  13990  fprodn0  14082  fprodsplitsn  14092  fprodle  14099  eftlcl  14210  reeftlcl  14211  rpnnen2lem6  14321  dvdsext  14405  3dvds  14418  gcdcllem3  14524  seq1st  14579  dvdslcm  14612  lcmeq0  14614  lcmcl  14615  lcmneg  14617  lcmdvds  14622  dvdsprime  14686  coprmgcdb  14703  pc2dvds  14877  prmpwdvds  14897  unbenlem  14901  infpnlem1  14903  1arith  14920  vdwmc2  14978  ramcl  15036  mrcuni  15576  isacs1i  15612  acsfn  15614  funcpropd  15854  natpropd  15930  curfcl  16166  curf2ndf  16181  resmhm  16655  resmhm2b  16657  mhmco  16658  mhmima  16659  pwsdiagmhm  16665  gsumwsubmcl  16671  gsumwspan  16679  grpissubg  16886  subgint  16890  ghmmhmb  16943  resghm  16948  cntzmhm  17041  symgextf1lem  17110  f1omvdconj  17136  pmtr3ncom  17165  dfod2  17264  gexdvds  17284  subgpgp  17298  sylow1lem3  17301  frgpnabllem1  17558  dprdfeq0  17704  isdrng2  18034  cntzsubr  18089  islmodd  18146  lsslss  18233  reslmhm2b  18326  psrbaglefi  18645  mptcoe1fsupp  18857  ply1coe  18938  ply1coeOLD  18939  psgnfix1  19215  psgndif  19219  zrhcopsgndif  19220  ocvocv  19283  frlmsslsp  19403  frlmlbs  19404  mamudi  19477  mamudir  19478  mat1dimelbas  19545  scmatmulcl  19592  scmatfo  19604  mulmarep1gsum2  19648  mdetunilem7  19692  mdetunilem9  19694  gsummatr01lem3  19731  smadiadetlem3  19742  mp2pm2mplem4  19882  chfacfisf  19927  chfacfisfcpmat  19928  cpmadugsumlemF  19949  elcls  20138  leordtval  20278  cnpnei  20329  cnco  20331  cnss1  20341  cmpsub  20464  hauscmplem  20470  dissnlocfin  20593  ptbasid  20639  tx2cn  20674  upxp  20687  txindis  20698  xkoptsub  20718  xkopt  20719  trfbas2  20907  filcon  20947  trfil2  20951  filssufilg  20975  ufileu  20983  fixufil  20986  ufilen  20994  rnelfmlem  21016  flimclsi  21042  hauspwpwf1  21051  fclsopn  21078  fclsfnflim  21091  fclscmpi  21093  alexsubALTlem3  21113  alexsubALTlem4  21114  ptcmplem5  21120  tgpmulg  21157  subgtgp  21169  tgpt0  21182  tsmsxplem2  21217  metss  21572  metustfbas  21621  dscopn  21637  xrsmopn  21879  cncfss  21980  icoopnst  22016  iccpnfcnv  22021  icccvx  22027  evth  22036  phtpycc  22071  pcohtpylem  22099  lmmbrf  22281  fgcfil  22290  caucfil  22302  cfilres  22315  bcth3  22348  ovolfioo  22469  ovolficc  22470  voliunlem3  22554  volcn  22613  mbflimsup  22672  mbflimsupOLD  22673  mbfi1fseqlem5  22726  itg2seq  22749  dvnff  22926  dvnadd  22932  cpnord  22938  c1liplem1  22997  plypf1  23215  plyaddlem1  23216  plymullem1  23217  coeeulem  23227  coeidlem  23240  dgrle  23246  dgrnznn  23250  plycjlem  23279  elqaalem3  23323  elqaalem3OLD  23326  ulmcaulem  23398  ulmcau  23399  psergf  23416  psercn2  23427  efopn  23652  abscxpbnd  23742  leibpi  23917  isppw2  24091  muinv  24171  bposlem3  24263  pntrmax  24451  pntpbnd1  24473  qabvexp  24513  eqeelen  24983  colinearalglem4  24988  axcgrid  24995  axsegconlem1  24996  axsegconlem3  24998  ax5seglem1  25007  ax5seglem2  25008  ax5seglem9  25016  axcontlem2  25044  usgraidx2vlem2  25168  cusgrares  25249  cusgrafilem2  25257  wlkiswwlk1  25467  wwlkextproplem3  25520  el2wlkonot  25646  el2spthonot0  25648  usgravd00  25696  rusgraprop4  25721  eupath2lem3  25756  frgrancvvdeqlemB  25815  frgrawopreglem5  25825  frghash2spot  25840  numclwwlkovf2ex  25863  grpoidinvlem3  25983  grpoidinv  25985  grpoideu  25986  subgoablo  26088  nmoub3i  26463  nmlno0lem  26483  nmlnoubi  26486  ipasslem3  26523  ipblnfi  26546  hvaddsub4  26780  his35  26790  shsel3  27017  chj4  27237  spansncol  27270  chscllem2  27340  5oalem2  27357  3oalem2  27365  hoaddcl  27460  adjsym  27535  cnvadj  27594  hhcno  27606  hhcnf  27607  nmopub2tALT  27611  unoplin  27622  counop  27623  nmfnleub2  27628  hmoplin  27644  brafnmul  27653  nmlnop0iALT  27697  nmopun  27716  nmophmi  27733  riesz3i  27764  riesz1  27767  cnlnadjlem2  27770  cnlnadjlem6  27774  adjmul  27794  adjadd  27795  bra11  27810  cnvbraval  27812  kbass5  27822  kbass6  27823  leop2  27826  leopadd  27834  leopmuli  27835  leoptri  27838  leopnmid  27840  nmopleid  27841  pj3si  27909  hstel2  27921  cvcon3  27986  dmdmd  28002  dmdbr5  28010  mdsl0  28012  mdslmd1lem1  28027  mdslmd1lem2  28028  mdslmd3i  28034  superpos  28056  chirredlem2  28093  chirredlem3  28094  mdsymlem3  28107  mdsymlem5  28109  mdsymlem6  28110  sumdmdlem  28120  cdjreui  28134  cdj1i  28135  cdj3i  28143  foresf1o  28188  abfmpel  28303  fcomptf  28309  fcnvgreu  28324  xrge0infss  28389  xrge0infssOLD  28390  cmpcref  28726  xrge0iifcnv  28788  esumcst  28933  hasheuni  28955  esum2dlem  28962  esum2d  28963  sigaclcu2  28991  insiga  29008  unelldsys  29029  measres  29093  measdivcst  29096  volfiniune  29102  ddemeas  29108  sgn3da  29461  sconpi1  30011  cvmsss2  30046  mrsubco  30208  dfon2lem6  30483  dftrpred3g  30523  poseq  30540  soseq  30541  nodenselem3  30621  nobndlem6  30635  hfext  30999  elicc3  31022  fnessref  31062  fin2solem  31976  fin2so  31977  poimirlem2  31987  poimirlem14  31999  poimirlem25  32010  poimirlem26  32011  poimirlem29  32014  poimirlem30  32015  broucube  32019  heicant  32020  mblfinlem2  32023  mblfinlem3  32024  mblfinlem4  32025  ex-ovoliunnfl  32028  mbfresfi  32032  cnambfre  32034  itg2addnclem  32038  itg2addnclem2  32039  itg2addnc  32041  bddiblnc  32057  ftc1anclem3  32064  ftc1anclem4  32065  ftc1anclem5  32066  ftc1anclem6  32067  ftc1anclem7  32068  ftc1anclem8  32069  ftc1anc  32070  eqfnun  32093  indexdom  32106  filbcmb  32112  fzadd2  32115  fdc  32119  incsequz  32122  metf1o  32129  caures  32134  bndss  32163  ismtycnv  32179  heiborlem1  32188  rrncmslem  32209  isdrngo2  32242  rngoisocnv  32265  unichnidl  32309  ax12eq  32557  ax12el  32558  lshpset2N  32730  pmapglb2N  33381  pmapglb2xN  33382  pclfinN  33510  polval2N  33516  cdleme31fv2  34005  cdleme32fvcl  34052  cdleme48gfv  34149  tendoicl  34408  tendoipl  34409  diaglbN  34668  dochkr1  35091  dochkr1OLDN  35092  nacsfix  35599  eq0rabdioph  35664  diophren  35701  rencldnfilem  35708  pell1234qrdich  35752  jm2.24  35858  bezoutr1  35881  jm2.26lem3  35901  wepwsolem  35945  pwssplit4  35992  isnumbasgrplem3  36009  cvgdvgrat  36706  ofsubid  36717  bcc0  36733  binomcxplemnn0  36742  uzwo4  37430  fiiuncl  37444  disjrnmpt2  37501  fompt  37505  disjinfi  37506  mapsnd  37514  choicefi  37519  ssfiunibd  37565  supxrgelem  37598  suplesup  37600  xrlexaddrp  37613  xralrple2  37615  fsumsplitsn  37687  fsumsupp0  37695  divcnvg  37745  limcrecl  37747  sumnnodd  37748  islpcn  37757  lptre2pt  37758  limcresiooub  37761  limcresioolb  37762  limclner  37770  cncfuni  37802  icccncfext  37803  cncficcgt0  37804  cncfiooicclem1  37809  cncfiooiccre  37811  dvasinbx  37830  dvdsn1add  37852  dvnmul  37856  dvmptfprodlem  37857  dvnprodlem1  37859  dvnprodlem3  37861  iblspltprt  37888  itgioocnicc  37892  itgspltprt  37894  stirlinglem5  37978  dirker2re  37992  dirkerper  37996  dirkertrigeq  38001  dirkercncflem2  38004  fourierdlem12  38019  fourierdlem15  38022  fourierdlem16  38023  fourierdlem20  38027  fourierdlem21  38028  fourierdlem22  38029  fourierdlem39  38047  fourierdlem40  38048  fourierdlem41  38049  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem46  38054  fourierdlem49  38057  fourierdlem50  38058  fourierdlem57  38065  fourierdlem58  38066  fourierdlem59  38067  fourierdlem64  38072  fourierdlem65  38073  fourierdlem66  38074  fourierdlem68  38076  fourierdlem70  38078  fourierdlem71  38079  fourierdlem73  38081  fourierdlem78  38086  fourierdlem79  38087  fourierdlem80  38088  fourierdlem81  38089  fourierdlem82  38090  fourierdlem83  38091  fourierdlem87  38095  fourierdlem93  38101  fourierdlem95  38103  fourierdlem101  38109  fourierdlem103  38111  fourierdlem104  38112  fourierdlem111  38119  fourierdlem112  38120  sqwvfoura  38130  fourierswlem  38132  elaa2lem  38135  elaa2lemOLD  38136  etransclem13  38150  etransclem23  38160  etransclem24  38161  etransclem32  38169  etransclem38  38175  etransclem46  38183  qndenserrnbllem  38201  prsal  38217  intsal  38227  salexct  38231  dfsalgen2  38238  sge0rnre  38244  sge0val  38246  sge0z  38255  sge0revalmpt  38258  sge0tsms  38260  sge0pr  38274  sge0resplit  38286  sge0split  38289  sge0splitmpt  38291  sge0iunmptlemfi  38293  sge0iunmptlemre  38295  sge0fodjrnlem  38296  sge0iunmpt  38298  sge0rpcpnf  38301  sge0ltfirpmpt2  38306  sge0isum  38307  sge0xaddlem1  38313  sge0xaddlem2  38314  sge0pnffsumgt  38322  sge0gtfsumgt  38323  nnfoctbdjlem  38331  nnfoctbdj  38332  meadjun  38338  meadjiunlem  38341  omeiunltfirp  38378  carageniuncllem2  38381  caratheodorylem1  38385  caratheodorylem2  38386  caratheodory  38387  isomenndlem  38389  isomennd  38390  hoicvr  38408  volicorescl  38413  ovnsubaddlem2  38431  hoidmvlelem2  38456  hoidmvlelem3  38457  hoidmvle  38460  ovnhoilem2  38462  hspdifhsp  38476  hoiqssbllem2  38483  hoiqssbllem3  38484  hspmbllem2  38487  smonoord  38756  bgoldbst  38917  lswn0  38960  2f1fvneq  39054  f1cofveqaeq  39055  egrsubgr  39399  cusgrfilem2  39567  uspgrn2crct  39826  usgra2pthlem1  39940  vdcusgra  39946  resmgmhm  40071  resmgmhm2b  40073  mgmhmco  40074  mgmhmima  40075  snlindsntorlem  40536  aacllem  40813
  Copyright terms: Public domain W3C validator