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

Theorem adantll 695
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 448 . 2  |-  ( ( th  /\  ph )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 458 1  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  ad2antlr  708  ad2ant2l  727  ad2ant2lr  729  3ad2antl3  1121  3adant1l  1176  ax11eq  2220  ax11el  2221  nfeud2  2243  ralcom2  2808  reu6  3059  sbc2iegf  3163  sbcralt  3169  pofun  4453  tz7.7  4541  onfr  4554  limsssuc  4763  poinxp  4874  sossfld  5250  ssimaex  5720  fndmdif  5766  dffo4  5817  foco2  5821  fcompt  5836  fconst2g  5878  isores3  5987  curry1  6370  curry2  6373  onnseq  6535  oe0  6695  oesuclem  6698  oecl  6710  oaordi  6718  oawordri  6722  oaass  6733  omordi  6738  omword2  6746  omlimcl  6750  odi  6751  omass  6752  oeoe  6771  nnaordi  6790  oaabs  6816  omsmolem  6825  eceqoveq  6938  dom2lem  7076  sbthlem9  7154  php3  7222  onomeneq  7225  isinf  7251  frfi  7281  fiint  7312  fodomfib  7315  fofinf1o  7316  marypha1lem  7366  ordiso2  7410  unwdomg  7478  xpwdomg  7479  ac5num  7843  cff1  8064  cfcoflem  8078  infpssrlem4  8112  isf32lem9  8167  isf34lem7  8185  fin1a2lem13  8218  fin1a2s  8220  hsmexlem4  8235  axdc2lem  8254  zorn2lem6  8307  inttsk  8575  tskuni  8584  nqereu  8732  prcdnq  8796  addclprlem2  8820  ltexpri  8846  prlem936  8850  reclem2pr  8851  axsup  9077  add4  9206  ltleadd  9436  lt2mul2div  9811  lediv12a  9828  infmrcl  9912  nn2ge  9950  zextle  10268  fnn0ind  10294  xrlttr  10658  ifle  10708  xaddass  10753  xmulasslem3  10790  xlemul1a  10792  xadddilem  10798  xrsupsslem  10810  xrinfmsslem  10811  supxrunb1  10823  supxrunb2  10824  ixxin  10858  difreicc  10953  iccsplit  10954  iccshftr  10955  iccshftl  10957  iccdil  10959  icccntr  10961  fzaddel  11012  fzrev  11032  modadd1  11198  modmul1  11199  mulexp  11339  expadd  11342  expmul  11345  leexp1a  11358  expnbnd  11428  bccl  11533  hashdom  11573  hashfacen  11623  revccat  11718  2shfti  11815  cau3lem  12078  subcn2  12308  caucvgb  12393  iseraltlem1  12395  sumss  12438  incexclem  12536  supcvg  12555  mertenslem2  12582  eftlcl  12628  reeftlcl  12629  rpnnen2lem6  12739  dvdsext  12820  3dvds  12832  gcdcllem3  12933  seq1st  12982  dvdsprime  13012  pc2dvds  13172  prmpwdvds  13192  unbenlem  13196  infpnlem1  13198  1arith  13215  vdwmc2  13267  ramcl  13317  mrcuni  13766  isacs1i  13802  acsfn  13804  funcpropd  14017  natpropd  14093  curfcl  14249  curf2ndf  14264  spwpr2  14580  resmhm  14679  resmhm2b  14681  mhmco  14682  mhmima  14683  pwsdiagmhm  14688  gsumwsubmcl  14704  gsumwspan  14711  subgint  14884  ghmmhmb  14937  resghm  14942  cntzmhm  15057  dfod2  15120  gexdvds  15138  subgpgp  15151  sylow1lem3  15154  frgpnabllem1  15404  dprdfeq0  15500  isdrng2  15765  cntzsubr  15820  islmodd  15876  lsslss  15957  reslmhm2b  16050  psrbaglefi  16357  ply1coe  16604  ocvocv  16814  elcls  17053  leordtval  17192  cnpnei  17243  cnco  17245  cnss1  17255  cmpsub  17378  hauscmplem  17384  ptbasid  17521  tx2cn  17556  upxp  17569  txindis  17580  xkoptsub  17600  xkopt  17601  trfbas2  17789  filcon  17829  trfil2  17833  filssufilg  17857  ufileu  17865  fixufil  17868  ufilen  17876  rnelfmlem  17898  flimclsi  17924  hauspwpwf1  17933  fclsopn  17960  fclsfnflim  17973  fclscmpi  17975  alexsubALTlem3  17994  alexsubALTlem4  17995  ptcmplem5  18001  tgpmulg  18037  subgtgp  18049  tgpt0  18062  tsmsxplem2  18097  metss  18421  metustfbas  18470  dscopn  18485  xrsmopn  18707  cncfss  18793  icoopnst  18828  iccpnfcnv  18833  icccvx  18839  evth  18848  phtpycc  18880  pcohtpylem  18908  lmmbrf  19079  fgcfil  19088  caucfil  19100  cfilres  19113  bcth3  19146  ovolfioo  19224  ovolficc  19225  voliunlem3  19306  volcn  19358  mbflimsup  19418  mbfi1fseqlem5  19471  itg2seq  19494  dvnff  19669  dvnadd  19675  cpnord  19681  c1liplem1  19740  plypf1  19991  plyaddlem1  19992  plymullem1  19993  coeeulem  20003  coeidlem  20016  dgrle  20022  plycjlem  20054  elqaalem3  20098  ulmcaulem  20170  ulmcau  20171  psergf  20188  psercn2  20199  efopn  20409  abscxpbnd  20497  leibpi  20642  isppw2  20758  muinv  20838  bposlem3  20930  pntrmax  21118  pntpbnd1  21140  qabvexp  21180  usgraidx2vlem2  21270  cusgrares  21340  cusgrafilem2  21348  eupath2lem3  21542  grpoidinvlem3  21635  grpoidinv  21637  grpoideu  21638  subgoablo  21740  nmoub3i  22115  nmlno0lem  22135  nmlnoubi  22138  ipasslem3  22175  ipblnfi  22198  hvaddsub4  22421  his35  22431  shsel3  22658  chj4  22878  spansncol  22911  chscllem2  22981  5oalem2  22998  3oalem2  23006  hoaddcl  23102  adjsym  23177  cnvadj  23236  hhcno  23248  hhcnf  23249  nmopub2tALT  23253  unoplin  23264  counop  23265  nmfnleub2  23270  hmoplin  23286  brafnmul  23295  nmlnop0iALT  23339  nmopun  23358  nmophmi  23375  riesz3i  23406  riesz1  23409  cnlnadjlem2  23412  cnlnadjlem6  23416  adjmul  23436  adjadd  23437  bra11  23452  cnvbraval  23454  kbass5  23464  kbass6  23465  leop2  23468  leopadd  23476  leopmuli  23477  leoptri  23480  leopnmid  23482  nmopleid  23483  pj3si  23551  hstel2  23563  cvcon3  23628  dmdmd  23644  dmdbr5  23652  mdsl0  23654  mdslmd1lem1  23669  mdslmd1lem2  23670  mdslmd3i  23676  superpos  23698  chirredlem2  23735  chirredlem3  23736  mdsymlem3  23749  mdsymlem5  23751  mdsymlem6  23752  sumdmdlem  23762  cdjreui  23776  cdj1i  23777  cdj3i  23785  abfmpel  23902  fcomptf  23912  xrge0iifcnv  24116  esumcst  24244  hasheuni  24264  sigaclcu2  24292  insiga  24309  measres  24363  measdivcst  24366  volfiniune  24373  sconpi1  24698  cvmsss2  24733  fprodn0  25075  dfon2lem6  25161  predpo  25201  preddowncl  25213  dftrpred3g  25253  poseq  25270  soseq  25271  nodenselem3  25354  nobndlem6  25368  eqeelen  25550  colinearalglem4  25555  axcgrid  25562  axsegconlem1  25563  axsegconlem3  25565  ax5seglem1  25574  ax5seglem2  25575  ax5seglem9  25583  axcontlem2  25611  hfext  25831  ex-ovoliunnfl  25947  itg2addnclem2  25951  itg2addnc  25952  bddiblnc  25968  elicc3  26004  fnessref  26057  eqfnun  26107  indexdom  26120  filbcmb  26126  fzadd2  26129  fdc  26133  incsequz  26136  metf1o  26145  caures  26150  bndss  26179  ismtycnv  26195  heiborlem1  26204  rrncmslem  26225  isdrngo2  26258  rngoisocnv  26281  unichnidl  26325  nacsfix  26450  eq0rabdioph  26519  diophren  26558  rencldnfilem  26565  pell1234qrdich  26608  jm2.24  26712  bezoutr1  26735  jm2.26lem3  26756  wepwsolem  26800  pwssplit4  26853  frlmsslsp  26910  frlmlbs  26911  isnumbasgrplem3  26932  dgrnznn  27002  f1omvdconj  27051  mamudi  27123  mamudir  27124  ofsubid  27203  stirlinglem5  27488  frgrancvvdeqlemB  27783  frgrawopreglem5  27793  lshpset2N  29285  pmapglb2N  29936  pmapglb2xN  29937  pclfinN  30065  polval2N  30071  cdleme31fv2  30558  cdleme32fvcl  30605  cdleme48gfv  30702  tendoicl  30961  tendoipl  30962  diaglbN  31221  dochkr1  31644  dochkr1OLDN  31645
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator