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

Theorem adantll 713
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 461 . 2  |-  ( ( th  /\  ph )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 471 1  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )
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:  ad2antlr  726  ad2ant2l  745  ad2ant2lr  747  3ad2antl3  1161  3adant1l  1221  ax12eq  2257  ax12el  2258  ralcom2  3008  reu6  3274  sbc2iegf  3388  sbcralt  3394  pofun  4806  tz7.7  4894  onfr  4907  poinxp  5053  xpdifid  5425  sossfld  5444  ssimaex  5923  fndmdif  5976  dffo4  6032  foco2  6036  fcompt  6052  fconst2g  6110  isores3  6216  limsssuc  6670  curry1  6877  curry2  6880  extmptsuppeq  6926  suppss  6932  suppssov1  6934  suppss2  6936  suppssfv  6938  onnseq  7017  oe0  7174  oesuclem  7177  oecl  7189  oaordi  7197  oawordri  7201  oaass  7212  omordi  7217  omword2  7225  omlimcl  7229  odi  7230  omass  7231  oeoe  7250  nnaordi  7269  oaabs  7295  omsmolem  7304  eceqoveq  7418  dom2lem  7557  sbthlem9  7637  php3  7705  onomeneq  7709  isinf  7735  frfi  7767  fiint  7799  fodomfib  7802  fofinf1o  7803  marypha1lem  7895  ordiso2  7943  unwdomg  8013  xpwdomg  8014  ac5num  8420  cff1  8641  cfcoflem  8655  infpssrlem4  8689  isf32lem9  8744  isf34lem7  8762  fin1a2lem13  8795  fin1a2s  8797  hsmexlem4  8812  axdc2lem  8831  zorn2lem6  8884  axpowndlem2  8976  inttsk  9155  tskuni  9164  nqereu  9310  prcdnq  9374  addclprlem2  9398  ltexpri  9424  prlem936  9428  reclem2pr  9429  axsup  9663  add4  9799  ltleadd  10041  lt2mul2div  10427  lediv12a  10444  infmrcl  10528  nn2ge  10567  zextle  10942  fnn0ind  10968  xrlttr  11355  ifle  11405  xaddass  11450  xmulasslem3  11487  xlemul1a  11489  xadddilem  11495  xrsupsslem  11507  xrinfmsslem  11508  supxrunb1  11520  supxrunb2  11521  ixxin  11555  difreicc  11661  iccsplit  11662  iccshftr  11663  iccshftl  11665  iccdil  11667  icccntr  11669  fzaddel  11727  fzrev  11751  modadd1  12012  modmul1  12019  mulexp  12184  expadd  12187  expmul  12190  leexp1a  12203  expnbnd  12274  bccl  12379  hashdom  12426  hashfacen  12482  swrdccat3blem  12699  revccat  12719  2shfti  12892  rexico  13165  cau3lem  13166  subcn2  13396  caucvgb  13481  iseraltlem1  13483  sumss  13525  incexclem  13627  supcvg  13646  mertenslem2  13673  eftlcl  13719  reeftlcl  13720  rpnnen2lem6  13830  dvdsext  13914  3dvds  13927  gcdcllem3  14028  seq1st  14077  dvdsprime  14107  pc2dvds  14279  prmpwdvds  14299  unbenlem  14303  infpnlem1  14305  1arith  14322  vdwmc2  14374  ramcl  14424  mrcuni  14895  isacs1i  14931  acsfn  14933  funcpropd  15143  natpropd  15219  curfcl  15375  curf2ndf  15390  resmhm  15864  resmhm2b  15866  mhmco  15867  mhmima  15868  pwsdiagmhm  15874  gsumwsubmcl  15880  gsumwspan  15888  grpissubg  16095  subgint  16099  ghmmhmb  16152  resghm  16157  cntzmhm  16250  symgextf1lem  16319  f1omvdconj  16345  pmtr3ncom  16374  dfod2  16460  gexdvds  16478  subgpgp  16491  sylow1lem3  16494  frgpnabllem1  16751  dprdfeq0  16936  dprdfeq0OLD  16943  isdrng2  17280  cntzsubr  17335  islmodd  17392  lsslss  17481  reslmhm2b  17574  psrbaglefi  17897  psrbaglefiOLD  17898  mptcoe1fsupp  18129  ply1coe  18211  ply1coeOLD  18212  psgnfix1  18507  psgndif  18511  zrhcopsgndif  18512  ocvocv  18575  frlmsslsp  18702  frlmsslspOLD  18703  frlmlbs  18704  mamudi  18778  mamudir  18779  mat1dimelbas  18846  scmatmulcl  18893  scmatfo  18905  mulmarep1gsum2  18949  mdetunilem7  18993  mdetunilem9  18995  gsummatr01lem3  19032  smadiadetlem3  19043  mp2pm2mplem4  19183  chfacfisf  19228  chfacfisfcpmat  19229  cpmadugsumlemF  19250  elcls  19447  leordtval  19587  cnpnei  19638  cnco  19640  cnss1  19650  cmpsub  19773  hauscmplem  19779  dissnlocfin  19903  ptbasid  19949  tx2cn  19984  upxp  19997  txindis  20008  xkoptsub  20028  xkopt  20029  trfbas2  20217  filcon  20257  trfil2  20261  filssufilg  20285  ufileu  20293  fixufil  20296  ufilen  20304  rnelfmlem  20326  flimclsi  20352  hauspwpwf1  20361  fclsopn  20388  fclsfnflim  20401  fclscmpi  20403  alexsubALTlem3  20422  alexsubALTlem4  20423  ptcmplem5  20429  tgpmulg  20465  subgtgp  20477  tgpt0  20490  tsmsxplem2  20529  metss  20884  metustfbasOLD  20941  metustfbas  20942  dscopn  20967  xrsmopn  21190  cncfss  21276  icoopnst  21312  iccpnfcnv  21317  icccvx  21323  evth  21332  phtpycc  21364  pcohtpylem  21392  lmmbrf  21574  fgcfil  21583  caucfil  21595  cfilres  21608  bcth3  21643  ovolfioo  21752  ovolficc  21753  voliunlem3  21835  volcn  21888  mbflimsup  21946  mbfi1fseqlem5  21999  itg2seq  22022  dvnff  22199  dvnadd  22205  cpnord  22211  c1liplem1  22270  plypf1  22482  plyaddlem1  22483  plymullem1  22484  coeeulem  22494  coeidlem  22507  dgrle  22513  plycjlem  22545  elqaalem3  22589  ulmcaulem  22661  ulmcau  22662  psergf  22679  psercn2  22690  efopn  22911  abscxpbnd  22999  leibpi  23145  isppw2  23261  muinv  23341  bposlem3  23433  pntrmax  23621  pntpbnd1  23643  qabvexp  23683  eqeelen  24079  colinearalglem4  24084  axcgrid  24091  axsegconlem1  24092  axsegconlem3  24094  ax5seglem1  24103  ax5seglem2  24104  ax5seglem9  24112  axcontlem2  24140  usgraidx2vlem2  24264  cusgrares  24344  cusgrafilem2  24352  wlkiswwlk1  24562  wwlkextproplem3  24615  el2wlkonot  24741  el2spthonot0  24743  usgravd00  24791  rusgraprop4  24816  eupath2lem3  24851  frgrancvvdeqlemB  24910  frgrawopreglem5  24920  frghash2spot  24935  numclwwlkovf2ex  24958  grpoidinvlem3  25080  grpoidinv  25082  grpoideu  25083  subgoablo  25185  nmoub3i  25560  nmlno0lem  25580  nmlnoubi  25583  ipasslem3  25620  ipblnfi  25643  hvaddsub4  25867  his35  25877  shsel3  26105  chj4  26325  spansncol  26358  chscllem2  26428  5oalem2  26445  3oalem2  26453  hoaddcl  26549  adjsym  26624  cnvadj  26683  hhcno  26695  hhcnf  26696  nmopub2tALT  26700  unoplin  26711  counop  26712  nmfnleub2  26717  hmoplin  26733  brafnmul  26742  nmlnop0iALT  26786  nmopun  26805  nmophmi  26822  riesz3i  26853  riesz1  26856  cnlnadjlem2  26859  cnlnadjlem6  26863  adjmul  26883  adjadd  26884  bra11  26899  cnvbraval  26901  kbass5  26911  kbass6  26912  leop2  26915  leopadd  26923  leopmuli  26924  leoptri  26927  leopnmid  26929  nmopleid  26930  pj3si  26998  hstel2  27010  cvcon3  27075  dmdmd  27091  dmdbr5  27099  mdsl0  27101  mdslmd1lem1  27116  mdslmd1lem2  27117  mdslmd3i  27123  superpos  27145  chirredlem2  27182  chirredlem3  27183  mdsymlem3  27196  mdsymlem5  27198  mdsymlem6  27199  sumdmdlem  27209  cdjreui  27223  cdj1i  27224  cdj3i  27232  foresf1o  27275  abfmpel  27365  fcomptf  27375  fcnvgreu  27386  xrge0infss  27452  cmpcref  27726  xrge0iifcnv  27788  esumcst  27944  hasheuni  27964  sigaclcu2  27993  insiga  28010  measres  28066  measdivcst  28069  volfiniune  28075  ddemeas  28081  sgn3da  28353  sconpi1  28557  cvmsss2  28592  mrsubco  28754  fprodn0  29084  dfon2lem6  29195  predpo  29239  preddowncl  29251  dftrpred3g  29291  poseq  29308  soseq  29309  nodenselem3  29418  nobndlem6  29432  hfext  29815  fin2solem  30014  fin2so  30015  heicant  30024  mblfinlem2  30027  mblfinlem3  30028  mblfinlem4  30029  ex-ovoliunnfl  30032  mbfresfi  30036  cnambfre  30038  itg2addnclem  30041  itg2addnclem2  30042  itg2addnc  30044  bddiblnc  30060  ftc1anclem3  30067  ftc1anclem4  30068  ftc1anclem5  30069  ftc1anclem6  30070  ftc1anclem7  30071  ftc1anclem8  30072  ftc1anc  30073  elicc3  30110  fnessref  30150  eqfnun  30187  indexdom  30200  filbcmb  30206  fzadd2  30209  fdc  30213  incsequz  30216  metf1o  30223  caures  30228  bndss  30257  ismtycnv  30273  heiborlem1  30282  rrncmslem  30303  isdrngo2  30336  rngoisocnv  30359  unichnidl  30403  nacsfix  30619  eq0rabdioph  30685  diophren  30722  rencldnfilem  30729  pell1234qrdich  30772  jm2.24  30876  bezoutr1  30899  jm2.26lem3  30918  wepwsolem  30962  pwssplit4  31010  isnumbasgrplem3  31029  dgrnznn  31060  cvgdvgrat  31170  dvdslcm  31180  lcmeq0  31182  lcmcl  31183  lcmneg  31185  lcmdvds  31190  ofsubid  31205  ssfiunibd  31458  divcnvg  31541  limcrecl  31543  sumnnodd  31544  islpcn  31553  lptre2pt  31554  limcresiooub  31556  limcresioolb  31557  limclner  31565  cncfuni  31596  icccncfext  31597  cncficcgt0  31598  cncfiooicclem1  31603  cncfiooiccre  31605  dvasinbx  31621  iblspltprt  31662  itgioocnicc  31666  itgspltprt  31668  stirlinglem5  31749  dirker2re  31763  dirkerper  31767  dirkertrigeq  31772  dirkercncflem2  31775  fourierdlem12  31790  fourierdlem15  31793  fourierdlem16  31794  fourierdlem20  31798  fourierdlem21  31799  fourierdlem22  31800  fourierdlem39  31817  fourierdlem40  31818  fourierdlem41  31819  fourierdlem42  31820  fourierdlem46  31824  fourierdlem49  31827  fourierdlem50  31828  fourierdlem57  31835  fourierdlem58  31836  fourierdlem59  31837  fourierdlem64  31842  fourierdlem65  31843  fourierdlem66  31844  fourierdlem68  31846  fourierdlem70  31848  fourierdlem71  31849  fourierdlem73  31851  fourierdlem78  31856  fourierdlem79  31857  fourierdlem80  31858  fourierdlem81  31859  fourierdlem82  31860  fourierdlem83  31861  fourierdlem87  31865  fourierdlem93  31871  fourierdlem95  31873  fourierdlem101  31879  fourierdlem103  31881  fourierdlem104  31882  fourierdlem111  31889  fourierdlem112  31890  sqwvfoura  31900  fourierswlem  31902  2f1fvneq  32145  lswn0  32181  usgra2pthlem1  32191  vdcusgra  32197  resmgmhm  32324  resmgmhm2b  32326  mgmhmco  32327  mgmhmima  32328  snlindsntorlem  32806  lshpset2N  34584  pmapglb2N  35235  pmapglb2xN  35236  pclfinN  35364  polval2N  35370  cdleme31fv2  35859  cdleme32fvcl  35906  cdleme48gfv  36003  tendoicl  36262  tendoipl  36263  diaglbN  36522  dochkr1  36945  dochkr1OLDN  36946
  Copyright terms: Public domain W3C validator