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

Theorem adantll 696
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 449 . 2  |-  ( ( th  /\  ph )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 459 1  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  ad2antlr  709  ad2ant2l  728  ad2ant2lr  730  3ad2antl3  1122  3adant1l  1177  ax11eq  2276  ax11el  2277  nfeud2  2299  ralcom2  2878  reu6  3129  sbc2iegf  3240  sbcralt  3246  pofun  4548  tz7.7  4636  onfr  4649  limsssuc  4859  poinxp  4970  sossfld  5346  ssimaex  5817  fndmdif  5863  dffo4  5914  foco2  5918  fcompt  5933  fconst2g  5975  isores3  6084  curry1  6467  curry2  6470  onnseq  6635  oe0  6795  oesuclem  6798  oecl  6810  oaordi  6818  oawordri  6822  oaass  6833  omordi  6838  omword2  6846  omlimcl  6850  odi  6851  omass  6852  oeoe  6871  nnaordi  6890  oaabs  6916  omsmolem  6925  eceqoveq  7038  dom2lem  7176  sbthlem9  7254  php3  7322  onomeneq  7325  isinf  7351  frfi  7381  fiint  7412  fodomfib  7415  fofinf1o  7416  marypha1lem  7467  ordiso2  7513  unwdomg  7581  xpwdomg  7582  ac5num  7948  cff1  8169  cfcoflem  8183  infpssrlem4  8217  isf32lem9  8272  isf34lem7  8290  fin1a2lem13  8323  fin1a2s  8325  hsmexlem4  8340  axdc2lem  8359  zorn2lem6  8412  inttsk  8680  tskuni  8689  nqereu  8837  prcdnq  8901  addclprlem2  8925  ltexpri  8951  prlem936  8955  reclem2pr  8956  axsup  9182  add4  9312  ltleadd  9542  lt2mul2div  9917  lediv12a  9934  infmrcl  10018  nn2ge  10056  zextle  10374  fnn0ind  10400  xrlttr  10764  ifle  10814  xaddass  10859  xmulasslem3  10896  xlemul1a  10898  xadddilem  10904  xrsupsslem  10916  xrinfmsslem  10917  supxrunb1  10929  supxrunb2  10930  ixxin  10964  difreicc  11059  iccsplit  11060  iccshftr  11061  iccshftl  11063  iccdil  11065  icccntr  11067  fzaddel  11118  fzrev  11139  modadd1  11309  modmul1  11310  mulexp  11450  expadd  11453  expmul  11456  leexp1a  11469  expnbnd  11539  bccl  11644  hashdom  11684  hashfacen  11734  revccat  11829  2shfti  11926  cau3lem  12189  subcn2  12419  caucvgb  12504  iseraltlem1  12506  sumss  12549  incexclem  12647  supcvg  12666  mertenslem2  12693  eftlcl  12739  reeftlcl  12740  rpnnen2lem6  12850  dvdsext  12931  3dvds  12943  gcdcllem3  13044  seq1st  13093  dvdsprime  13123  pc2dvds  13283  prmpwdvds  13303  unbenlem  13307  infpnlem1  13309  1arith  13326  vdwmc2  13378  ramcl  13428  mrcuni  13877  isacs1i  13913  acsfn  13915  funcpropd  14128  natpropd  14204  curfcl  14360  curf2ndf  14375  spwpr2  14691  resmhm  14790  resmhm2b  14792  mhmco  14793  mhmima  14794  pwsdiagmhm  14799  gsumwsubmcl  14815  gsumwspan  14822  subgint  14995  ghmmhmb  15048  resghm  15053  cntzmhm  15168  dfod2  15231  gexdvds  15249  subgpgp  15262  sylow1lem3  15265  frgpnabllem1  15515  dprdfeq0  15611  isdrng2  15876  cntzsubr  15931  islmodd  15987  lsslss  16068  reslmhm2b  16161  psrbaglefi  16468  ply1coe  16715  ocvocv  16929  elcls  17168  leordtval  17308  cnpnei  17359  cnco  17361  cnss1  17371  cmpsub  17494  hauscmplem  17500  ptbasid  17638  tx2cn  17673  upxp  17686  txindis  17697  xkoptsub  17717  xkopt  17718  trfbas2  17906  filcon  17946  trfil2  17950  filssufilg  17974  ufileu  17982  fixufil  17985  ufilen  17993  rnelfmlem  18015  flimclsi  18041  hauspwpwf1  18050  fclsopn  18077  fclsfnflim  18090  fclscmpi  18092  alexsubALTlem3  18111  alexsubALTlem4  18112  ptcmplem5  18118  tgpmulg  18154  subgtgp  18166  tgpt0  18179  tsmsxplem2  18214  metss  18569  metustfbasOLD  18626  metustfbas  18627  dscopn  18652  xrsmopn  18874  cncfss  18960  icoopnst  18995  iccpnfcnv  19000  icccvx  19006  evth  19015  phtpycc  19047  pcohtpylem  19075  lmmbrf  19246  fgcfil  19255  caucfil  19267  cfilres  19280  bcth3  19315  ovolfioo  19395  ovolficc  19396  voliunlem3  19477  volcn  19529  mbflimsup  19587  mbfi1fseqlem5  19640  itg2seq  19663  dvnff  19840  dvnadd  19846  cpnord  19852  c1liplem1  19911  plypf1  20162  plyaddlem1  20163  plymullem1  20164  coeeulem  20174  coeidlem  20187  dgrle  20193  plycjlem  20225  elqaalem3  20269  ulmcaulem  20341  ulmcau  20342  psergf  20359  psercn2  20370  efopn  20580  abscxpbnd  20668  leibpi  20813  isppw2  20929  muinv  21009  bposlem3  21101  pntrmax  21289  pntpbnd1  21311  qabvexp  21351  usgraidx2vlem2  21442  cusgrares  21512  cusgrafilem2  21520  eupath2lem3  21732  grpoidinvlem3  21825  grpoidinv  21827  grpoideu  21828  subgoablo  21930  nmoub3i  22305  nmlno0lem  22325  nmlnoubi  22328  ipasslem3  22365  ipblnfi  22388  hvaddsub4  22611  his35  22621  shsel3  22848  chj4  23068  spansncol  23101  chscllem2  23171  5oalem2  23188  3oalem2  23196  hoaddcl  23292  adjsym  23367  cnvadj  23426  hhcno  23438  hhcnf  23439  nmopub2tALT  23443  unoplin  23454  counop  23455  nmfnleub2  23460  hmoplin  23476  brafnmul  23485  nmlnop0iALT  23529  nmopun  23548  nmophmi  23565  riesz3i  23596  riesz1  23599  cnlnadjlem2  23602  cnlnadjlem6  23606  adjmul  23626  adjadd  23627  bra11  23642  cnvbraval  23644  kbass5  23654  kbass6  23655  leop2  23658  leopadd  23666  leopmuli  23667  leoptri  23670  leopnmid  23672  nmopleid  23673  pj3si  23741  hstel2  23753  cvcon3  23818  dmdmd  23834  dmdbr5  23842  mdsl0  23844  mdslmd1lem1  23859  mdslmd1lem2  23860  mdslmd3i  23866  superpos  23888  chirredlem2  23925  chirredlem3  23926  mdsymlem3  23939  mdsymlem5  23941  mdsymlem6  23942  sumdmdlem  23952  cdjreui  23966  cdj1i  23967  cdj3i  23975  abfmpel  24098  fcomptf  24108  xrge0iifcnv  24350  esumcst  24486  hasheuni  24506  sigaclcu2  24534  insiga  24551  measres  24607  measdivcst  24610  volfiniune  24617  sconpi1  24957  cvmsss2  24992  fprodn0  25334  dfon2lem6  25446  predpo  25490  preddowncl  25502  dftrpred3g  25542  poseq  25559  soseq  25560  nodenselem3  25669  nobndlem6  25683  eqeelen  25874  colinearalglem4  25879  axcgrid  25886  axsegconlem1  25887  axsegconlem3  25889  ax5seglem1  25898  ax5seglem2  25899  ax5seglem9  25907  axcontlem2  25935  hfext  26155  heicant  26277  mblfinlem2  26280  mblfinlem3  26281  mblfinlem4  26282  ex-ovoliunnfl  26285  mbfresfi  26289  cnambfre  26291  itg2addnclem  26294  itg2addnclem2  26295  itg2addnc  26297  bddiblnc  26313  ftc1anclem3  26320  ftc1anclem4  26321  ftc1anclem5  26322  ftc1anclem6  26323  ftc1anclem7  26324  ftc1anclem8  26325  ftc1anc  26326  elicc3  26358  fnessref  26411  eqfnun  26461  indexdom  26474  filbcmb  26480  fzadd2  26483  fdc  26487  incsequz  26490  metf1o  26499  caures  26504  bndss  26533  ismtycnv  26549  heiborlem1  26558  rrncmslem  26579  isdrngo2  26612  rngoisocnv  26635  unichnidl  26679  nacsfix  26804  eq0rabdioph  26873  diophren  26912  rencldnfilem  26919  pell1234qrdich  26962  jm2.24  27066  bezoutr1  27089  jm2.26lem3  27110  wepwsolem  27154  pwssplit4  27206  frlmsslsp  27263  frlmlbs  27264  isnumbasgrplem3  27285  dgrnznn  27355  f1omvdconj  27404  mamudi  27476  mamudir  27477  ofsubid  27556  stirlinglem5  27841  2f1fvneq  28119  swrdccat3blem  28276  2cshw1lem1  28306  lswrdn0  28318  usgra2pthlem1  28372  wlkiswwlk1  28396  el2wlkonot  28425  el2spthonot0  28427  vdcusgra  28453  usgravd00  28460  frgrancvvdeqlemB  28525  frgrawopreglem5  28535  frghash2spot  28550  lshpset2N  30015  pmapglb2N  30666  pmapglb2xN  30667  pclfinN  30795  polval2N  30801  cdleme31fv2  31288  cdleme32fvcl  31335  cdleme48gfv  31432  tendoicl  31691  tendoipl  31692  diaglbN  31951  dochkr1  32374  dochkr1OLDN  32375
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 179  df-an 362
  Copyright terms: Public domain W3C validator