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  1152  3adant1l  1211  ax12eq  2251  ax12el  2252  nfeud2OLD  2289  ralcom2  2991  reu6  3255  sbc2iegf  3369  sbcralt  3375  pofun  4766  tz7.7  4854  onfr  4867  poinxp  5011  xpdifid  5375  sossfld  5394  ssimaex  5866  fndmdif  5917  dffo4  5969  foco2  5973  fcompt  5989  fconst2g  6042  isores3  6136  limsssuc  6572  curry1  6775  curry2  6778  extmptsuppeq  6824  suppss  6830  suppssov1  6832  suppss2  6834  suppssfv  6836  onnseq  6916  oe0  7073  oesuclem  7076  oecl  7088  oaordi  7096  oawordri  7100  oaass  7111  omordi  7116  omword2  7124  omlimcl  7128  odi  7129  omass  7130  oeoe  7149  nnaordi  7168  oaabs  7194  omsmolem  7203  eceqoveq  7316  dom2lem  7460  sbthlem9  7540  php3  7608  onomeneq  7612  isinf  7638  frfi  7669  fiint  7700  fodomfib  7703  fofinf1o  7704  marypha1lem  7795  ordiso2  7841  unwdomg  7911  xpwdomg  7912  ac5num  8318  cff1  8539  cfcoflem  8553  infpssrlem4  8587  isf32lem9  8642  isf34lem7  8660  fin1a2lem13  8693  fin1a2s  8695  hsmexlem4  8710  axdc2lem  8729  zorn2lem6  8782  axpowndlem2  8874  inttsk  9053  tskuni  9062  nqereu  9210  prcdnq  9274  addclprlem2  9298  ltexpri  9324  prlem936  9328  reclem2pr  9329  axsup  9562  add4  9697  ltleadd  9934  lt2mul2div  10320  lediv12a  10337  infmrcl  10421  nn2ge  10459  zextle  10827  fnn0ind  10853  xrlttr  11229  ifle  11279  xaddass  11324  xmulasslem3  11361  xlemul1a  11363  xadddilem  11369  xrsupsslem  11381  xrinfmsslem  11382  supxrunb1  11394  supxrunb2  11395  ixxin  11429  difreicc  11535  iccsplit  11536  iccshftr  11537  iccshftl  11539  iccdil  11541  icccntr  11543  fzaddel  11611  fzrev  11637  modadd1  11863  modmul1  11870  mulexp  12021  expadd  12024  expmul  12027  leexp1a  12040  expnbnd  12111  bccl  12216  hashdom  12261  hashfacen  12326  swrdccat3blem  12505  revccat  12525  2shfti  12688  cau3lem  12961  subcn2  13191  caucvgb  13276  iseraltlem1  13278  sumss  13320  incexclem  13418  supcvg  13437  mertenslem2  13464  eftlcl  13510  reeftlcl  13511  rpnnen2lem6  13621  dvdsext  13703  3dvds  13715  gcdcllem3  13816  seq1st  13865  dvdsprime  13895  pc2dvds  14064  prmpwdvds  14084  unbenlem  14088  infpnlem1  14090  1arith  14107  vdwmc2  14159  ramcl  14209  mrcuni  14679  isacs1i  14715  acsfn  14717  funcpropd  14930  natpropd  15006  curfcl  15162  curf2ndf  15177  resmhm  15607  resmhm2b  15609  mhmco  15610  mhmima  15611  pwsdiagmhm  15617  gsumwsubmcl  15636  gsumwspan  15644  grpissubg  15821  subgint  15825  ghmmhmb  15878  resghm  15883  cntzmhm  15976  symgextf1lem  16045  f1omvdconj  16072  pmtr3ncom  16101  dfod2  16187  gexdvds  16205  subgpgp  16218  sylow1lem3  16221  frgpnabllem1  16473  dprdfeq0  16635  dprdfeq0OLD  16642  isdrng2  16966  cntzsubr  17021  islmodd  17078  lsslss  17166  reslmhm2b  17259  psrbaglefi  17565  psrbaglefiOLD  17566  ply1coe  17872  ply1coeOLD  17873  psgnfix1  18154  psgndif  18158  zrhcopsgndif  18159  ocvocv  18222  frlmsslsp  18349  frlmsslspOLD  18350  frlmlbs  18351  mamudi  18433  mamudir  18434  mulmarep1gsum2  18513  mdetunilem7  18557  mdetunilem9  18559  gsummatr01lem3  18596  smadiadetlem3  18607  elcls  18810  leordtval  18950  cnpnei  19001  cnco  19003  cnss1  19013  cmpsub  19136  hauscmplem  19142  ptbasid  19281  tx2cn  19316  upxp  19329  txindis  19340  xkoptsub  19360  xkopt  19361  trfbas2  19549  filcon  19589  trfil2  19593  filssufilg  19617  ufileu  19625  fixufil  19628  ufilen  19636  rnelfmlem  19658  flimclsi  19684  hauspwpwf1  19693  fclsopn  19720  fclsfnflim  19733  fclscmpi  19735  alexsubALTlem3  19754  alexsubALTlem4  19755  ptcmplem5  19761  tgpmulg  19797  subgtgp  19809  tgpt0  19822  tsmsxplem2  19861  metss  20216  metustfbasOLD  20273  metustfbas  20274  dscopn  20299  xrsmopn  20522  cncfss  20608  icoopnst  20644  iccpnfcnv  20649  icccvx  20655  evth  20664  phtpycc  20696  pcohtpylem  20724  lmmbrf  20906  fgcfil  20915  caucfil  20927  cfilres  20940  bcth3  20975  ovolfioo  21084  ovolficc  21085  voliunlem3  21167  volcn  21220  mbflimsup  21278  mbfi1fseqlem5  21331  itg2seq  21354  dvnff  21531  dvnadd  21537  cpnord  21543  c1liplem1  21602  plypf1  21814  plyaddlem1  21815  plymullem1  21816  coeeulem  21826  coeidlem  21839  dgrle  21845  plycjlem  21877  elqaalem3  21921  ulmcaulem  21993  ulmcau  21994  psergf  22011  psercn2  22022  efopn  22237  abscxpbnd  22325  leibpi  22471  isppw2  22587  muinv  22667  bposlem3  22759  pntrmax  22947  pntpbnd1  22969  qabvexp  23009  eqeelen  23303  colinearalglem4  23308  axcgrid  23315  axsegconlem1  23316  axsegconlem3  23318  ax5seglem1  23327  ax5seglem2  23328  ax5seglem9  23336  axcontlem2  23364  usgraidx2vlem2  23463  cusgrares  23533  cusgrafilem2  23541  eupath2lem3  23753  grpoidinvlem3  23846  grpoidinv  23848  grpoideu  23849  subgoablo  23951  nmoub3i  24326  nmlno0lem  24346  nmlnoubi  24349  ipasslem3  24386  ipblnfi  24409  hvaddsub4  24633  his35  24643  shsel3  24871  chj4  25091  spansncol  25124  chscllem2  25194  5oalem2  25211  3oalem2  25219  hoaddcl  25315  adjsym  25390  cnvadj  25449  hhcno  25461  hhcnf  25462  nmopub2tALT  25466  unoplin  25477  counop  25478  nmfnleub2  25483  hmoplin  25499  brafnmul  25508  nmlnop0iALT  25552  nmopun  25571  nmophmi  25588  riesz3i  25619  riesz1  25622  cnlnadjlem2  25625  cnlnadjlem6  25629  adjmul  25649  adjadd  25650  bra11  25665  cnvbraval  25667  kbass5  25677  kbass6  25678  leop2  25681  leopadd  25689  leopmuli  25690  leoptri  25693  leopnmid  25695  nmopleid  25696  pj3si  25764  hstel2  25776  cvcon3  25841  dmdmd  25857  dmdbr5  25865  mdsl0  25867  mdslmd1lem1  25882  mdslmd1lem2  25883  mdslmd3i  25889  superpos  25911  chirredlem2  25948  chirredlem3  25949  mdsymlem3  25962  mdsymlem5  25964  mdsymlem6  25965  sumdmdlem  25975  cdjreui  25989  cdj1i  25990  cdj3i  25998  abfmpel  26122  fcomptf  26132  fcnvgreu  26143  xrge0infss  26205  xrge0iifcnv  26509  esumcst  26660  hasheuni  26680  sigaclcu2  26709  insiga  26726  measres  26782  measdivcst  26785  volfiniune  26791  ddemeas  26797  sgn3da  27069  sconpi1  27273  cvmsss2  27308  fprodn0  27635  dfon2lem6  27746  predpo  27790  preddowncl  27802  dftrpred3g  27842  poseq  27859  soseq  27860  nodenselem3  27969  nobndlem6  27983  hfext  28366  fin2solem  28564  fin2so  28565  heicant  28575  mblfinlem2  28578  mblfinlem3  28579  mblfinlem4  28580  ex-ovoliunnfl  28583  mbfresfi  28587  cnambfre  28589  itg2addnclem  28592  itg2addnclem2  28593  itg2addnc  28595  bddiblnc  28611  ftc1anclem3  28618  ftc1anclem4  28619  ftc1anclem5  28620  ftc1anclem6  28621  ftc1anclem7  28622  ftc1anclem8  28623  ftc1anc  28624  elicc3  28661  fnessref  28714  eqfnun  28764  indexdom  28777  filbcmb  28783  fzadd2  28786  fdc  28790  incsequz  28793  metf1o  28800  caures  28805  bndss  28834  ismtycnv  28850  heiborlem1  28859  rrncmslem  28880  isdrngo2  28913  rngoisocnv  28936  unichnidl  28980  nacsfix  29197  eq0rabdioph  29264  diophren  29301  rencldnfilem  29308  pell1234qrdich  29351  jm2.24  29455  bezoutr1  29478  jm2.26lem3  29499  wepwsolem  29543  pwssplit4  29591  isnumbasgrplem3  29610  dgrnznn  29641  ofsubid  29747  stirlinglem5  30022  2f1fvneq  30292  lswn0  30407  usgra2pthlem1  30449  wlkiswwlk1  30473  el2wlkonot  30537  el2spthonot0  30539  vdcusgra  30680  usgravd00  30687  rusgraprop4  30705  wwlkextproplem3  30711  frgrancvvdeqlemB  30780  frgrawopreglem5  30790  frghash2spot  30805  numclwwlkovf2ex  30828  mptcoe1fsupp  30987  mat1dimelbas  31034  snlindsntorlem  31137  mp2pm2mplem4  31297  chfacfisf  31341  chfacfisfcpmat  31342  cpmadugsumlemF  31363  lshpset2N  33103  pmapglb2N  33754  pmapglb2xN  33755  pclfinN  33883  polval2N  33889  cdleme31fv2  34376  cdleme32fvcl  34423  cdleme48gfv  34520  tendoicl  34779  tendoipl  34780  diaglbN  35039  dochkr1  35462  dochkr1OLDN  35463
  Copyright terms: Public domain W3C validator