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  1160  3adant1l  1220  ax12eq  2264  ax12el  2265  nfeud2OLD  2302  ralcom2  3026  reu6  3292  sbc2iegf  3406  sbcralt  3412  pofun  4816  tz7.7  4904  onfr  4917  poinxp  5062  xpdifid  5433  sossfld  5452  ssimaex  5930  fndmdif  5983  dffo4  6035  foco2  6039  fcompt  6055  fconst2g  6113  isores3  6217  limsssuc  6663  curry1  6872  curry2  6875  extmptsuppeq  6921  suppss  6927  suppssov1  6929  suppss2  6931  suppssfv  6933  onnseq  7012  oe0  7169  oesuclem  7172  oecl  7184  oaordi  7192  oawordri  7196  oaass  7207  omordi  7212  omword2  7220  omlimcl  7224  odi  7225  omass  7226  oeoe  7245  nnaordi  7264  oaabs  7290  omsmolem  7299  eceqoveq  7413  dom2lem  7552  sbthlem9  7632  php3  7700  onomeneq  7704  isinf  7730  frfi  7761  fiint  7793  fodomfib  7796  fofinf1o  7797  marypha1lem  7889  ordiso2  7936  unwdomg  8006  xpwdomg  8007  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  9148  tskuni  9157  nqereu  9303  prcdnq  9367  addclprlem2  9391  ltexpri  9417  prlem936  9421  reclem2pr  9422  axsup  9656  add4  9791  ltleadd  10031  lt2mul2div  10417  lediv12a  10434  infmrcl  10518  nn2ge  10557  zextle  10930  fnn0ind  10956  xrlttr  11342  ifle  11392  xaddass  11437  xmulasslem3  11474  xlemul1a  11476  xadddilem  11482  xrsupsslem  11494  xrinfmsslem  11495  supxrunb1  11507  supxrunb2  11508  ixxin  11542  difreicc  11648  iccsplit  11649  iccshftr  11650  iccshftl  11652  iccdil  11654  icccntr  11656  fzaddel  11714  fzrev  11738  modadd1  11997  modmul1  12004  mulexp  12169  expadd  12172  expmul  12175  leexp1a  12188  expnbnd  12259  bccl  12364  hashdom  12411  hashfacen  12465  swrdccat3blem  12679  revccat  12699  2shfti  12872  cau3lem  13146  subcn2  13376  caucvgb  13461  iseraltlem1  13463  sumss  13505  incexclem  13607  supcvg  13626  mertenslem2  13653  eftlcl  13699  reeftlcl  13700  rpnnen2lem6  13810  dvdsext  13892  3dvds  13905  gcdcllem3  14006  seq1st  14055  dvdsprime  14085  pc2dvds  14257  prmpwdvds  14277  unbenlem  14281  infpnlem1  14283  1arith  14300  vdwmc2  14352  ramcl  14402  mrcuni  14872  isacs1i  14908  acsfn  14910  funcpropd  15123  natpropd  15199  curfcl  15355  curf2ndf  15370  resmhm  15800  resmhm2b  15802  mhmco  15803  mhmima  15804  pwsdiagmhm  15810  gsumwsubmcl  15829  gsumwspan  15837  grpissubg  16016  subgint  16020  ghmmhmb  16073  resghm  16078  cntzmhm  16171  symgextf1lem  16240  f1omvdconj  16267  pmtr3ncom  16296  dfod2  16382  gexdvds  16400  subgpgp  16413  sylow1lem3  16416  frgpnabllem1  16668  dprdfeq0  16852  dprdfeq0OLD  16859  isdrng2  17189  cntzsubr  17244  islmodd  17301  lsslss  17390  reslmhm2b  17483  psrbaglefi  17794  psrbaglefiOLD  17795  mptcoe1fsupp  18026  ply1coe  18108  ply1coeOLD  18109  psgnfix1  18401  psgndif  18405  zrhcopsgndif  18406  ocvocv  18469  frlmsslsp  18596  frlmsslspOLD  18597  frlmlbs  18598  mamudi  18672  mamudir  18673  mat1dimelbas  18740  scmatmulcl  18787  scmatfo  18799  mulmarep1gsum2  18843  mdetunilem7  18887  mdetunilem9  18889  gsummatr01lem3  18926  smadiadetlem3  18937  mp2pm2mplem4  19077  chfacfisf  19122  chfacfisfcpmat  19123  cpmadugsumlemF  19144  elcls  19340  leordtval  19480  cnpnei  19531  cnco  19533  cnss1  19543  cmpsub  19666  hauscmplem  19672  ptbasid  19811  tx2cn  19846  upxp  19859  txindis  19870  xkoptsub  19890  xkopt  19891  trfbas2  20079  filcon  20119  trfil2  20123  filssufilg  20147  ufileu  20155  fixufil  20158  ufilen  20166  rnelfmlem  20188  flimclsi  20214  hauspwpwf1  20223  fclsopn  20250  fclsfnflim  20263  fclscmpi  20265  alexsubALTlem3  20284  alexsubALTlem4  20285  ptcmplem5  20291  tgpmulg  20327  subgtgp  20339  tgpt0  20352  tsmsxplem2  20391  metss  20746  metustfbasOLD  20803  metustfbas  20804  dscopn  20829  xrsmopn  21052  cncfss  21138  icoopnst  21174  iccpnfcnv  21179  icccvx  21185  evth  21194  phtpycc  21226  pcohtpylem  21254  lmmbrf  21436  fgcfil  21445  caucfil  21457  cfilres  21470  bcth3  21505  ovolfioo  21614  ovolficc  21615  voliunlem3  21697  volcn  21750  mbflimsup  21808  mbfi1fseqlem5  21861  itg2seq  21884  dvnff  22061  dvnadd  22067  cpnord  22073  c1liplem1  22132  plypf1  22344  plyaddlem1  22345  plymullem1  22346  coeeulem  22356  coeidlem  22369  dgrle  22375  plycjlem  22407  elqaalem3  22451  ulmcaulem  22523  ulmcau  22524  psergf  22541  psercn2  22552  efopn  22767  abscxpbnd  22855  leibpi  23001  isppw2  23117  muinv  23197  bposlem3  23289  pntrmax  23477  pntpbnd1  23499  qabvexp  23539  eqeelen  23883  colinearalglem4  23888  axcgrid  23895  axsegconlem1  23896  axsegconlem3  23898  ax5seglem1  23907  ax5seglem2  23908  ax5seglem9  23916  axcontlem2  23944  usgraidx2vlem2  24068  cusgrares  24148  cusgrafilem2  24156  wlkiswwlk1  24366  wwlkextproplem3  24419  el2wlkonot  24545  el2spthonot0  24547  usgravd00  24595  rusgraprop4  24620  eupath2lem3  24655  frgrancvvdeqlemB  24715  frgrawopreglem5  24725  frghash2spot  24740  numclwwlkovf2ex  24763  grpoidinvlem3  24884  grpoidinv  24886  grpoideu  24887  subgoablo  24989  nmoub3i  25364  nmlno0lem  25384  nmlnoubi  25387  ipasslem3  25424  ipblnfi  25447  hvaddsub4  25671  his35  25681  shsel3  25909  chj4  26129  spansncol  26162  chscllem2  26232  5oalem2  26249  3oalem2  26257  hoaddcl  26353  adjsym  26428  cnvadj  26487  hhcno  26499  hhcnf  26500  nmopub2tALT  26504  unoplin  26515  counop  26516  nmfnleub2  26521  hmoplin  26537  brafnmul  26546  nmlnop0iALT  26590  nmopun  26609  nmophmi  26626  riesz3i  26657  riesz1  26660  cnlnadjlem2  26663  cnlnadjlem6  26667  adjmul  26687  adjadd  26688  bra11  26703  cnvbraval  26705  kbass5  26715  kbass6  26716  leop2  26719  leopadd  26727  leopmuli  26728  leoptri  26731  leopnmid  26733  nmopleid  26734  pj3si  26802  hstel2  26814  cvcon3  26879  dmdmd  26895  dmdbr5  26903  mdsl0  26905  mdslmd1lem1  26920  mdslmd1lem2  26921  mdslmd3i  26927  superpos  26949  chirredlem2  26986  chirredlem3  26987  mdsymlem3  27000  mdsymlem5  27002  mdsymlem6  27003  sumdmdlem  27013  cdjreui  27027  cdj1i  27028  cdj3i  27036  abfmpel  27165  fcomptf  27175  fcnvgreu  27186  xrge0infss  27248  xrge0iifcnv  27551  esumcst  27711  hasheuni  27731  sigaclcu2  27760  insiga  27777  measres  27833  measdivcst  27836  volfiniune  27842  ddemeas  27848  sgn3da  28120  sconpi1  28324  cvmsss2  28359  fprodn0  28686  dfon2lem6  28797  predpo  28841  preddowncl  28853  dftrpred3g  28893  poseq  28910  soseq  28911  nodenselem3  29020  nobndlem6  29034  hfext  29417  fin2solem  29616  fin2so  29617  heicant  29626  mblfinlem2  29629  mblfinlem3  29630  mblfinlem4  29631  ex-ovoliunnfl  29634  mbfresfi  29638  cnambfre  29640  itg2addnclem  29643  itg2addnclem2  29644  itg2addnc  29646  bddiblnc  29662  ftc1anclem3  29669  ftc1anclem4  29670  ftc1anclem5  29671  ftc1anclem6  29672  ftc1anclem7  29673  ftc1anclem8  29674  ftc1anc  29675  elicc3  29712  fnessref  29765  eqfnun  29815  indexdom  29828  filbcmb  29834  fzadd2  29837  fdc  29841  incsequz  29844  metf1o  29851  caures  29856  bndss  29885  ismtycnv  29901  heiborlem1  29910  rrncmslem  29931  isdrngo2  29964  rngoisocnv  29987  unichnidl  30031  nacsfix  30248  eq0rabdioph  30314  diophren  30351  rencldnfilem  30358  pell1234qrdich  30401  jm2.24  30505  bezoutr1  30528  jm2.26lem3  30547  wepwsolem  30591  pwssplit4  30639  isnumbasgrplem3  30658  dgrnznn  30689  dvdslcm  30804  lcmeq0  30806  lcmcl  30807  lcmneg  30809  lcmdvds  30814  ofsubid  30829  ssfiunibd  31086  divcnvg  31169  limcrecl  31171  sumnnodd  31172  islpcn  31181  lptre2pt  31182  limcresiooub  31184  limcresioolb  31185  limclner  31193  cncfshift  31212  cncfperiod  31217  cncfuni  31225  icccncfext  31226  cncficcgt0  31227  cncfiooiccre  31234  dvasinbx  31250  iblspltprt  31291  itgioocnicc  31295  itgspltprt  31297  stirlinglem5  31378  dirker2re  31392  dirkerval2  31394  dirkerper  31396  dirkertrigeq  31401  dirkercncflem2  31404  fourierdlem12  31419  fourierdlem15  31422  fourierdlem16  31423  fourierdlem20  31427  fourierdlem21  31428  fourierdlem22  31429  fourierdlem34  31441  fourierdlem39  31446  fourierdlem40  31447  fourierdlem41  31448  fourierdlem42  31449  fourierdlem46  31453  fourierdlem49  31456  fourierdlem50  31457  fourierdlem57  31464  fourierdlem58  31465  fourierdlem59  31466  fourierdlem64  31471  fourierdlem65  31472  fourierdlem66  31473  fourierdlem68  31475  fourierdlem70  31477  fourierdlem71  31478  fourierdlem73  31480  fourierdlem78  31485  fourierdlem79  31486  fourierdlem80  31487  fourierdlem81  31488  fourierdlem82  31489  fourierdlem83  31490  fourierdlem87  31494  fourierdlem93  31500  fourierdlem95  31502  fourierdlem101  31508  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  sqwvfoura  31529  fourierswlem  31531  2f1fvneq  31776  lswn0  31812  usgra2pthlem1  31822  vdcusgra  31828  snlindsntorlem  32144  lshpset2N  33916  pmapglb2N  34567  pmapglb2xN  34568  pclfinN  34696  polval2N  34702  cdleme31fv2  35189  cdleme32fvcl  35236  cdleme48gfv  35333  tendoicl  35592  tendoipl  35593  diaglbN  35852  dochkr1  36275  dochkr1OLDN  36276
  Copyright terms: Public domain W3C validator