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  2927  reu6  3197  sbc2iegf  3304  sbcralt  3310  pofun  4728  poinxp  4855  xpdifid  5222  sossfld  5240  predpo  5355  preddowncl  5364  tz7.7  5406  onfr  5419  ssimaex  5885  fndmdif  5940  dffo4  5992  foco2  5996  fcompt  6013  fconst2g  6073  isores3  6180  limsssuc  6630  curry1  6838  curry2  6841  extmptsuppeq  6889  suppss  6895  suppssov1  6897  suppss2  6899  suppssfv  6901  onnseq  7013  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  7558  sbthlem9  7638  php3  7706  onomeneq  7710  isinf  7733  frfi  7764  fiint  7796  fodomfib  7799  fofinf1o  7800  marypha1lem  7895  ordiso2  7978  unwdomg  8047  xpwdomg  8048  ac5num  8413  cff1  8634  cfcoflem  8648  infpssrlem4  8682  isf32lem9  8737  isf34lem7  8755  fin1a2lem13  8788  fin1a2s  8790  hsmexlem4  8805  axdc2lem  8824  zorn2lem6  8877  axpowndlem2  8969  inttsk  9145  tskuni  9154  nqereu  9300  prcdnq  9364  addclprlem2  9388  ltexpri  9414  prlem936  9418  reclem2pr  9419  axsup  9655  add4  9795  ltleadd  10043  lt2mul2div  10429  lediv12a  10445  infmrclOLD  10539  nn2ge  10580  zextle  10955  fnn0ind  10980  xrlttr  11385  ifle  11436  xaddass  11481  xmulasslem3  11518  xlemul1a  11520  xadddilem  11526  xrsupsslem  11538  xrinfmsslem  11539  supxrunb1  11551  supxrunb2  11552  ixxin  11598  difreicc  11710  iccsplit  11711  iccshftr  11712  iccshftl  11714  iccdil  11716  icccntr  11718  fzaddel  11779  fzrev  11804  modadd1  12079  modmul1  12088  mulexp  12256  expadd  12259  expmul  12262  leexp1a  12276  expnbnd  12346  bccl  12452  hashdom  12503  hashfacen  12560  brfi1uzind  12594  wrdnval  12640  swrdccat3blem  12792  revccat  12812  2shfti  13082  rexico  13355  cau3lem  13356  subcn2  13596  caucvgb  13684  iseraltlem1  13686  sumss  13728  incexclem  13832  supcvg  13852  mertenslem2  13879  fprodn0  13971  fprodsplitsn  13981  fprodle  13988  eftlcl  14099  reeftlcl  14100  rpnnen2lem6  14210  dvdsext  14294  3dvds  14307  gcdcllem3  14413  seq1st  14468  dvdslcm  14501  lcmeq0  14503  lcmcl  14504  lcmneg  14506  lcmdvds  14511  dvdsprime  14575  coprmgcdb  14592  pc2dvds  14766  prmpwdvds  14786  unbenlem  14790  infpnlem1  14792  1arith  14809  vdwmc2  14867  ramcl  14925  mrcuni  15465  isacs1i  15501  acsfn  15503  funcpropd  15743  natpropd  15819  curfcl  16055  curf2ndf  16070  resmhm  16544  resmhm2b  16546  mhmco  16547  mhmima  16548  pwsdiagmhm  16554  gsumwsubmcl  16560  gsumwspan  16568  grpissubg  16775  subgint  16779  ghmmhmb  16832  resghm  16837  cntzmhm  16930  symgextf1lem  16999  f1omvdconj  17025  pmtr3ncom  17054  dfod2  17153  gexdvds  17173  subgpgp  17187  sylow1lem3  17190  frgpnabllem1  17447  dprdfeq0  17593  isdrng2  17923  cntzsubr  17978  islmodd  18035  lsslss  18122  reslmhm2b  18215  psrbaglefi  18534  mptcoe1fsupp  18746  ply1coe  18827  ply1coeOLD  18828  psgnfix1  19103  psgndif  19107  zrhcopsgndif  19108  ocvocv  19171  frlmsslsp  19291  frlmlbs  19292  mamudi  19365  mamudir  19366  mat1dimelbas  19433  scmatmulcl  19480  scmatfo  19492  mulmarep1gsum2  19536  mdetunilem7  19580  mdetunilem9  19582  gsummatr01lem3  19619  smadiadetlem3  19630  mp2pm2mplem4  19770  chfacfisf  19815  chfacfisfcpmat  19816  cpmadugsumlemF  19837  elcls  20026  leordtval  20166  cnpnei  20217  cnco  20219  cnss1  20229  cmpsub  20352  hauscmplem  20358  dissnlocfin  20481  ptbasid  20527  tx2cn  20562  upxp  20575  txindis  20586  xkoptsub  20606  xkopt  20607  trfbas2  20795  filcon  20835  trfil2  20839  filssufilg  20863  ufileu  20871  fixufil  20874  ufilen  20882  rnelfmlem  20904  flimclsi  20930  hauspwpwf1  20939  fclsopn  20966  fclsfnflim  20979  fclscmpi  20981  alexsubALTlem3  21001  alexsubALTlem4  21002  ptcmplem5  21008  tgpmulg  21045  subgtgp  21057  tgpt0  21070  tsmsxplem2  21105  metss  21460  metustfbas  21509  dscopn  21525  xrsmopn  21767  cncfss  21868  icoopnst  21904  iccpnfcnv  21909  icccvx  21915  evth  21924  phtpycc  21959  pcohtpylem  21987  lmmbrf  22169  fgcfil  22178  caucfil  22190  cfilres  22203  bcth3  22236  ovolfioo  22357  ovolficc  22358  voliunlem3  22442  volcn  22501  mbflimsup  22560  mbflimsupOLD  22561  mbfi1fseqlem5  22614  itg2seq  22637  dvnff  22814  dvnadd  22820  cpnord  22826  c1liplem1  22885  plypf1  23103  plyaddlem1  23104  plymullem1  23105  coeeulem  23115  coeidlem  23128  dgrle  23134  dgrnznn  23138  plycjlem  23167  elqaalem3  23211  elqaalem3OLD  23214  ulmcaulem  23286  ulmcau  23287  psergf  23304  psercn2  23315  efopn  23540  abscxpbnd  23630  leibpi  23805  isppw2  23979  muinv  24059  bposlem3  24151  pntrmax  24339  pntpbnd1  24361  qabvexp  24401  eqeelen  24871  colinearalglem4  24876  axcgrid  24883  axsegconlem1  24884  axsegconlem3  24886  ax5seglem1  24895  ax5seglem2  24896  ax5seglem9  24904  axcontlem2  24932  usgraidx2vlem2  25056  cusgrares  25137  cusgrafilem2  25145  wlkiswwlk1  25355  wwlkextproplem3  25408  el2wlkonot  25534  el2spthonot0  25536  usgravd00  25584  rusgraprop4  25609  eupath2lem3  25644  frgrancvvdeqlemB  25703  frgrawopreglem5  25713  frghash2spot  25728  numclwwlkovf2ex  25751  grpoidinvlem3  25871  grpoidinv  25873  grpoideu  25874  subgoablo  25976  nmoub3i  26351  nmlno0lem  26371  nmlnoubi  26374  ipasslem3  26411  ipblnfi  26434  hvaddsub4  26668  his35  26678  shsel3  26905  chj4  27125  spansncol  27158  chscllem2  27228  5oalem2  27245  3oalem2  27253  hoaddcl  27348  adjsym  27423  cnvadj  27482  hhcno  27494  hhcnf  27495  nmopub2tALT  27499  unoplin  27510  counop  27511  nmfnleub2  27516  hmoplin  27532  brafnmul  27541  nmlnop0iALT  27585  nmopun  27604  nmophmi  27621  riesz3i  27652  riesz1  27655  cnlnadjlem2  27658  cnlnadjlem6  27662  adjmul  27682  adjadd  27683  bra11  27698  cnvbraval  27700  kbass5  27710  kbass6  27711  leop2  27714  leopadd  27722  leopmuli  27723  leoptri  27726  leopnmid  27728  nmopleid  27729  pj3si  27797  hstel2  27809  cvcon3  27874  dmdmd  27890  dmdbr5  27898  mdsl0  27900  mdslmd1lem1  27915  mdslmd1lem2  27916  mdslmd3i  27922  superpos  27944  chirredlem2  27981  chirredlem3  27982  mdsymlem3  27995  mdsymlem5  27997  mdsymlem6  27998  sumdmdlem  28008  cdjreui  28022  cdj1i  28023  cdj3i  28031  foresf1o  28077  abfmpel  28195  fcomptf  28201  fcnvgreu  28216  xrge0infss  28285  xrge0infssOLD  28286  cmpcref  28624  xrge0iifcnv  28686  esumcst  28831  hasheuni  28853  esum2dlem  28860  esum2d  28861  sigaclcu2  28889  insiga  28906  unelldsys  28927  measres  28991  measdivcst  28994  volfiniune  29000  ddemeas  29006  sgn3da  29359  sconpi1  29909  cvmsss2  29944  mrsubco  30106  dfon2lem6  30380  dftrpred3g  30420  poseq  30437  soseq  30438  nodenselem3  30516  nobndlem6  30530  hfext  30894  elicc3  30917  fnessref  30957  fin2solem  31838  fin2so  31839  poimirlem2  31849  poimirlem14  31861  poimirlem25  31872  poimirlem26  31873  poimirlem29  31876  poimirlem30  31877  broucube  31881  heicant  31882  mblfinlem2  31885  mblfinlem3  31886  mblfinlem4  31887  ex-ovoliunnfl  31890  mbfresfi  31894  cnambfre  31896  itg2addnclem  31900  itg2addnclem2  31901  itg2addnc  31903  bddiblnc  31919  ftc1anclem3  31926  ftc1anclem4  31927  ftc1anclem5  31928  ftc1anclem6  31929  ftc1anclem7  31930  ftc1anclem8  31931  ftc1anc  31932  eqfnun  31955  indexdom  31968  filbcmb  31974  fzadd2  31977  fdc  31981  incsequz  31984  metf1o  31991  caures  31996  bndss  32025  ismtycnv  32041  heiborlem1  32050  rrncmslem  32071  isdrngo2  32104  rngoisocnv  32127  unichnidl  32171  ax12eq  32424  ax12el  32425  lshpset2N  32597  pmapglb2N  33248  pmapglb2xN  33249  pclfinN  33377  polval2N  33383  cdleme31fv2  33872  cdleme32fvcl  33919  cdleme48gfv  34016  tendoicl  34275  tendoipl  34276  diaglbN  34535  dochkr1  34958  dochkr1OLDN  34959  nacsfix  35466  eq0rabdioph  35531  diophren  35568  rencldnfilem  35575  pell1234qrdich  35620  jm2.24  35726  bezoutr1  35749  jm2.26lem3  35769  wepwsolem  35813  pwssplit4  35860  isnumbasgrplem3  35877  cvgdvgrat  36575  ofsubid  36586  bcc0  36602  binomcxplemnn0  36611  uzwo4  37308  fiiuncl  37322  disjrnmpt2  37367  fompt  37371  disjinfi  37372  ssfiunibd  37424  supxrgelem  37457  suplesup  37459  xrlexaddrp  37472  xralrple2  37474  fsumsplitsn  37533  divcnvg  37590  limcrecl  37592  sumnnodd  37593  islpcn  37602  lptre2pt  37603  limcresiooub  37606  limcresioolb  37607  limclner  37615  cncfuni  37647  icccncfext  37648  cncficcgt0  37649  cncfiooicclem1  37654  cncfiooiccre  37656  dvasinbx  37675  dvdsn1add  37697  dvnmul  37701  dvmptfprodlem  37702  dvnprodlem1  37704  dvnprodlem3  37706  iblspltprt  37733  itgioocnicc  37737  itgspltprt  37739  stirlinglem5  37823  dirker2re  37837  dirkerper  37841  dirkertrigeq  37846  dirkercncflem2  37849  fourierdlem12  37864  fourierdlem15  37867  fourierdlem16  37868  fourierdlem20  37872  fourierdlem21  37873  fourierdlem22  37874  fourierdlem39  37892  fourierdlem40  37893  fourierdlem41  37894  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem46  37899  fourierdlem49  37902  fourierdlem50  37903  fourierdlem57  37910  fourierdlem58  37911  fourierdlem59  37912  fourierdlem64  37917  fourierdlem65  37918  fourierdlem66  37919  fourierdlem68  37921  fourierdlem70  37923  fourierdlem71  37924  fourierdlem73  37926  fourierdlem78  37931  fourierdlem79  37932  fourierdlem80  37933  fourierdlem81  37934  fourierdlem82  37935  fourierdlem83  37936  fourierdlem87  37940  fourierdlem93  37946  fourierdlem95  37948  fourierdlem101  37954  fourierdlem103  37956  fourierdlem104  37957  fourierdlem111  37964  fourierdlem112  37965  sqwvfoura  37975  fourierswlem  37977  elaa2lem  37980  elaa2lemOLD  37981  etransclem13  37995  etransclem23  38005  etransclem24  38006  etransclem32  38014  etransclem38  38020  etransclem46  38028  prsal  38043  intsal  38053  sge0rnre  38057  sge0val  38059  sge0z  38068  sge0revalmpt  38071  sge0tsms  38073  sge0pr  38087  sge0resplit  38099  sge0split  38102  sge0splitmpt  38104  sge0iunmptlemfi  38106  sge0iunmptlemre  38108  sge0fodjrnlem  38109  sge0iunmpt  38111  sge0rpcpnf  38114  sge0ltfirpmpt2  38119  sge0isum  38120  sge0xaddlem1  38126  sge0xaddlem2  38127  sge0pnffsumgt  38135  sge0gtfsumgt  38136  nnfoctbdjlem  38144  nnfoctbdj  38145  meadjun  38151  meadjiunlem  38154  omeiunltfirp  38191  carageniuncllem2  38194  caratheodorylem1  38198  caratheodorylem2  38199  caratheodory  38200  isomenndlem  38202  isomennd  38203  hoicvr  38217  volicorescl  38222  ovnsubaddlem2  38240  hoidmvlelem2  38265  hoidmvlelem3  38266  hoidmvle  38269  ovnhoilem2  38271  smonoord  38531  bgoldbst  38692  lswn0  38733  2f1fvneq  38820  cusgrfilem2  39245  usgra2pthlem1  39258  vdcusgra  39264  resmgmhm  39389  resmgmhm2b  39391  mgmhmco  39392  mgmhmima  39393  snlindsntorlem  39856  aacllem  40133
  Copyright terms: Public domain W3C validator