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

Theorem adantll 718
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 462 . 2  |-  ( ( th  /\  ph )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 473 1  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  ad2antlr  731  ad2ant2l  750  ad2ant2lr  752  3ad2antl3  1169  3adant1l  1256  ralcom2  3000  reu6  3266  sbc2iegf  3372  sbcralt  3378  pofun  4791  poinxp  4918  xpdifid  5285  sossfld  5303  predpo  5417  preddowncl  5426  tz7.7  5468  onfr  5481  ssimaex  5946  fndmdif  6001  dffo4  6053  foco2  6057  fcompt  6074  fconst2g  6134  isores3  6241  limsssuc  6691  curry1  6899  curry2  6902  extmptsuppeq  6950  suppss  6956  suppssov1  6958  suppss2  6960  suppssfv  6962  onnseq  7071  oe0  7232  oesuclem  7235  oecl  7247  oaordi  7255  oawordri  7259  oaass  7270  omordi  7275  omword2  7283  omlimcl  7287  odi  7288  omass  7289  oeoe  7308  nnaordi  7327  oaabs  7353  omsmolem  7362  eceqoveq  7476  dom2lem  7616  sbthlem9  7696  php3  7764  onomeneq  7768  isinf  7791  frfi  7822  fiint  7854  fodomfib  7857  fofinf1o  7858  marypha1lem  7953  ordiso2  8030  unwdomg  8099  xpwdomg  8100  ac5num  8465  cff1  8686  cfcoflem  8700  infpssrlem4  8734  isf32lem9  8789  isf34lem7  8807  fin1a2lem13  8840  fin1a2s  8842  hsmexlem4  8857  axdc2lem  8876  zorn2lem6  8929  axpowndlem2  9021  inttsk  9198  tskuni  9207  nqereu  9353  prcdnq  9417  addclprlem2  9441  ltexpri  9467  prlem936  9471  reclem2pr  9472  axsup  9708  add4  9848  ltleadd  10096  lt2mul2div  10482  lediv12a  10499  infmrclOLD  10593  nn2ge  10634  zextle  11009  fnn0ind  11034  xrlttr  11439  ifle  11490  xaddass  11535  xmulasslem3  11572  xlemul1a  11574  xadddilem  11580  xrsupsslem  11592  xrinfmsslem  11593  supxrunb1  11605  supxrunb2  11606  ixxin  11652  difreicc  11762  iccsplit  11763  iccshftr  11764  iccshftl  11766  iccdil  11768  icccntr  11770  fzaddel  11831  fzrev  11856  modadd1  12131  modmul1  12140  mulexp  12308  expadd  12311  expmul  12314  leexp1a  12328  expnbnd  12398  bccl  12504  hashdom  12555  hashfacen  12612  wrdnval  12684  swrdccat3blem  12836  revccat  12856  2shfti  13122  rexico  13395  cau3lem  13396  subcn2  13636  caucvgb  13724  iseraltlem1  13726  sumss  13768  incexclem  13872  supcvg  13892  mertenslem2  13919  fprodn0  14011  fprodsplitsn  14021  fprodle  14028  eftlcl  14139  reeftlcl  14140  rpnnen2lem6  14250  dvdsext  14334  3dvds  14347  gcdcllem3  14449  seq1st  14501  dvdslcm  14528  lcmeq0  14530  lcmcl  14531  lcmneg  14533  lcmdvds  14538  dvdsprime  14599  coprmgcdb  14616  pc2dvds  14782  prmpwdvds  14802  unbenlem  14806  infpnlem1  14808  1arith  14825  vdwmc2  14883  ramcl  14941  mrcuni  15469  isacs1i  15505  acsfn  15507  funcpropd  15747  natpropd  15823  curfcl  16059  curf2ndf  16074  resmhm  16548  resmhm2b  16550  mhmco  16551  mhmima  16552  pwsdiagmhm  16558  gsumwsubmcl  16564  gsumwspan  16572  grpissubg  16779  subgint  16783  ghmmhmb  16836  resghm  16841  cntzmhm  16934  symgextf1lem  17003  f1omvdconj  17029  pmtr3ncom  17058  dfod2  17144  gexdvds  17162  subgpgp  17175  sylow1lem3  17178  frgpnabllem1  17435  dprdfeq0  17581  isdrng2  17911  cntzsubr  17966  islmodd  18023  lsslss  18110  reslmhm2b  18203  psrbaglefi  18522  mptcoe1fsupp  18734  ply1coe  18815  ply1coeOLD  18816  psgnfix1  19088  psgndif  19092  zrhcopsgndif  19093  ocvocv  19156  frlmsslsp  19276  frlmlbs  19277  mamudi  19350  mamudir  19351  mat1dimelbas  19418  scmatmulcl  19465  scmatfo  19477  mulmarep1gsum2  19521  mdetunilem7  19565  mdetunilem9  19567  gsummatr01lem3  19604  smadiadetlem3  19615  mp2pm2mplem4  19755  chfacfisf  19800  chfacfisfcpmat  19801  cpmadugsumlemF  19822  elcls  20011  leordtval  20151  cnpnei  20202  cnco  20204  cnss1  20214  cmpsub  20337  hauscmplem  20343  dissnlocfin  20466  ptbasid  20512  tx2cn  20547  upxp  20560  txindis  20571  xkoptsub  20591  xkopt  20592  trfbas2  20780  filcon  20820  trfil2  20824  filssufilg  20848  ufileu  20856  fixufil  20859  ufilen  20867  rnelfmlem  20889  flimclsi  20915  hauspwpwf1  20924  fclsopn  20951  fclsfnflim  20964  fclscmpi  20966  alexsubALTlem3  20986  alexsubALTlem4  20987  ptcmplem5  20993  tgpmulg  21030  subgtgp  21042  tgpt0  21055  tsmsxplem2  21090  metss  21445  metustfbas  21494  dscopn  21510  xrsmopn  21732  cncfss  21818  icoopnst  21854  iccpnfcnv  21859  icccvx  21865  evth  21874  phtpycc  21906  pcohtpylem  21934  lmmbrf  22116  fgcfil  22125  caucfil  22137  cfilres  22150  bcth3  22183  ovolfioo  22290  ovolficc  22291  voliunlem3  22373  volcn  22432  mbflimsup  22491  mbflimsupOLD  22492  mbfi1fseqlem5  22545  itg2seq  22568  dvnff  22745  dvnadd  22751  cpnord  22757  c1liplem1  22816  plypf1  23025  plyaddlem1  23026  plymullem1  23027  coeeulem  23037  coeidlem  23050  dgrle  23056  dgrnznn  23060  plycjlem  23089  elqaalem3  23133  ulmcaulem  23205  ulmcau  23206  psergf  23223  psercn2  23234  efopn  23459  abscxpbnd  23549  leibpi  23724  isppw2  23896  muinv  23976  bposlem3  24068  pntrmax  24256  pntpbnd1  24278  qabvexp  24318  eqeelen  24771  colinearalglem4  24776  axcgrid  24783  axsegconlem1  24784  axsegconlem3  24786  ax5seglem1  24795  ax5seglem2  24796  ax5seglem9  24804  axcontlem2  24832  usgraidx2vlem2  24956  cusgrares  25036  cusgrafilem2  25044  wlkiswwlk1  25254  wwlkextproplem3  25307  el2wlkonot  25433  el2spthonot0  25435  usgravd00  25483  rusgraprop4  25508  eupath2lem3  25543  frgrancvvdeqlemB  25602  frgrawopreglem5  25612  frghash2spot  25627  numclwwlkovf2ex  25650  grpoidinvlem3  25770  grpoidinv  25772  grpoideu  25773  subgoablo  25875  nmoub3i  26250  nmlno0lem  26270  nmlnoubi  26273  ipasslem3  26310  ipblnfi  26333  hvaddsub4  26557  his35  26567  shsel3  26794  chj4  27014  spansncol  27047  chscllem2  27117  5oalem2  27134  3oalem2  27142  hoaddcl  27237  adjsym  27312  cnvadj  27371  hhcno  27383  hhcnf  27384  nmopub2tALT  27388  unoplin  27399  counop  27400  nmfnleub2  27405  hmoplin  27421  brafnmul  27430  nmlnop0iALT  27474  nmopun  27493  nmophmi  27510  riesz3i  27541  riesz1  27544  cnlnadjlem2  27547  cnlnadjlem6  27551  adjmul  27571  adjadd  27572  bra11  27587  cnvbraval  27589  kbass5  27599  kbass6  27600  leop2  27603  leopadd  27611  leopmuli  27612  leoptri  27615  leopnmid  27617  nmopleid  27618  pj3si  27686  hstel2  27698  cvcon3  27763  dmdmd  27779  dmdbr5  27787  mdsl0  27789  mdslmd1lem1  27804  mdslmd1lem2  27805  mdslmd3i  27811  superpos  27833  chirredlem2  27870  chirredlem3  27871  mdsymlem3  27884  mdsymlem5  27886  mdsymlem6  27887  sumdmdlem  27897  cdjreui  27911  cdj1i  27912  cdj3i  27920  foresf1o  27966  abfmpel  28085  fcomptf  28091  fcnvgreu  28106  xrge0infss  28172  cmpcref  28507  xrge0iifcnv  28569  esumcst  28714  hasheuni  28736  esum2dlem  28743  esum2d  28744  sigaclcu2  28772  insiga  28789  unelldsys  28810  measres  28874  measdivcst  28877  volfiniune  28883  ddemeas  28889  sgn3da  29191  sconpi1  29741  cvmsss2  29776  mrsubco  29938  dfon2lem6  30212  dftrpred3g  30252  poseq  30269  soseq  30270  nodenselem3  30348  nobndlem6  30362  hfext  30726  elicc3  30749  fnessref  30789  fin2solem  31625  fin2so  31626  poimirlem2  31636  poimirlem14  31648  poimirlem25  31659  poimirlem26  31660  poimirlem29  31663  poimirlem30  31664  broucube  31668  heicant  31669  mblfinlem2  31672  mblfinlem3  31673  mblfinlem4  31674  ex-ovoliunnfl  31677  mbfresfi  31681  cnambfre  31683  itg2addnclem  31687  itg2addnclem2  31688  itg2addnc  31690  bddiblnc  31706  ftc1anclem3  31713  ftc1anclem4  31714  ftc1anclem5  31715  ftc1anclem6  31716  ftc1anclem7  31717  ftc1anclem8  31718  ftc1anc  31719  eqfnun  31742  indexdom  31755  filbcmb  31761  fzadd2  31764  fdc  31768  incsequz  31771  metf1o  31778  caures  31783  bndss  31812  ismtycnv  31828  heiborlem1  31837  rrncmslem  31858  isdrngo2  31891  rngoisocnv  31914  unichnidl  31958  ax12eq  32211  ax12el  32212  lshpset2N  32384  pmapglb2N  33035  pmapglb2xN  33036  pclfinN  33164  polval2N  33170  cdleme31fv2  33659  cdleme32fvcl  33706  cdleme48gfv  33803  tendoicl  34062  tendoipl  34063  diaglbN  34322  dochkr1  34745  dochkr1OLDN  34746  nacsfix  35253  eq0rabdioph  35318  diophren  35355  rencldnfilem  35362  pell1234qrdich  35405  jm2.24  35509  bezoutr1  35532  jm2.26lem3  35552  wepwsolem  35596  pwssplit4  35643  isnumbasgrplem3  35660  cvgdvgrat  36289  ofsubid  36300  bcc0  36316  binomcxplemnn0  36325  uzwo4  37023  fiiuncl  37038  disjrnmpt2  37076  fompt  37080  disjinfi  37081  ssfiunibd  37126  supxrgelem  37159  suplesup  37161  fsumsplitsn  37214  divcnvg  37269  limcrecl  37271  sumnnodd  37272  islpcn  37281  lptre2pt  37282  limcresiooub  37285  limcresioolb  37286  limclner  37294  cncfuni  37326  icccncfext  37327  cncficcgt0  37328  cncfiooicclem1  37333  cncfiooiccre  37335  dvasinbx  37354  dvdsn1add  37373  dvnmul  37377  dvmptfprodlem  37378  dvnprodlem1  37380  dvnprodlem3  37382  iblspltprt  37409  itgioocnicc  37413  itgspltprt  37415  stirlinglem5  37499  dirker2re  37513  dirkerper  37517  dirkertrigeq  37522  dirkercncflem2  37525  fourierdlem12  37540  fourierdlem15  37543  fourierdlem16  37544  fourierdlem20  37548  fourierdlem21  37549  fourierdlem22  37550  fourierdlem39  37567  fourierdlem40  37568  fourierdlem41  37569  fourierdlem42  37570  fourierdlem46  37574  fourierdlem49  37577  fourierdlem50  37578  fourierdlem57  37585  fourierdlem58  37586  fourierdlem59  37587  fourierdlem64  37592  fourierdlem65  37593  fourierdlem66  37594  fourierdlem68  37596  fourierdlem70  37598  fourierdlem71  37599  fourierdlem73  37601  fourierdlem78  37606  fourierdlem79  37607  fourierdlem80  37608  fourierdlem81  37609  fourierdlem82  37610  fourierdlem83  37611  fourierdlem87  37615  fourierdlem93  37621  fourierdlem95  37623  fourierdlem101  37629  fourierdlem103  37631  fourierdlem104  37632  fourierdlem111  37639  fourierdlem112  37640  sqwvfoura  37650  fourierswlem  37652  elaa2lem  37655  etransclem13  37669  etransclem23  37679  etransclem24  37680  etransclem32  37688  etransclem38  37694  etransclem46  37702  prsal  37716  intsal  37726  sge0rnre  37730  sge0val  37732  sge0z  37741  sge0revalmpt  37744  sge0tsms  37746  sge0pr  37760  sge0resplit  37772  sge0split  37775  sge0splitmpt  37777  sge0iunmptlemfi  37779  sge0iunmptlemre  37781  sge0fodjrnlem  37782  sge0iunmpt  37784  nnfoctbdjlem  37792  nnfoctbdj  37793  meadjun  37799  meadjiunlem  37802  omeiunltfirp  37839  carageniuncllem2  37842  caratheodorylem1  37846  caratheodorylem2  37847  caratheodory  37848  smonoord  38098  bgoldbst  38259  lswn0  38300  2f1fvneq  38374  usgra2pthlem1  38413  vdcusgra  38419  resmgmhm  38546  resmgmhm2b  38548  mgmhmco  38549  mgmhmima  38550  snlindsntorlem  39013  aacllem  39291
  Copyright terms: Public domain W3C validator