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  2269  ax11el  2270  nfeud2  2292  ralcom2  2864  reu6  3115  sbc2iegf  3219  sbcralt  3225  pofun  4511  tz7.7  4599  onfr  4612  limsssuc  4821  poinxp  4932  sossfld  5308  ssimaex  5779  fndmdif  5825  dffo4  5876  foco2  5880  fcompt  5895  fconst2g  5937  isores3  6046  curry1  6429  curry2  6432  onnseq  6597  oe0  6757  oesuclem  6760  oecl  6772  oaordi  6780  oawordri  6784  oaass  6795  omordi  6800  omword2  6808  omlimcl  6812  odi  6813  omass  6814  oeoe  6833  nnaordi  6852  oaabs  6878  omsmolem  6887  eceqoveq  7000  dom2lem  7138  sbthlem9  7216  php3  7284  onomeneq  7287  isinf  7313  frfi  7343  fiint  7374  fodomfib  7377  fofinf1o  7378  marypha1lem  7429  ordiso2  7473  unwdomg  7541  xpwdomg  7542  ac5num  7906  cff1  8127  cfcoflem  8141  infpssrlem4  8175  isf32lem9  8230  isf34lem7  8248  fin1a2lem13  8281  fin1a2s  8283  hsmexlem4  8298  axdc2lem  8317  zorn2lem6  8370  inttsk  8638  tskuni  8647  nqereu  8795  prcdnq  8859  addclprlem2  8883  ltexpri  8909  prlem936  8913  reclem2pr  8914  axsup  9140  add4  9270  ltleadd  9500  lt2mul2div  9875  lediv12a  9892  infmrcl  9976  nn2ge  10014  zextle  10332  fnn0ind  10358  xrlttr  10722  ifle  10772  xaddass  10817  xmulasslem3  10854  xlemul1a  10856  xadddilem  10862  xrsupsslem  10874  xrinfmsslem  10875  supxrunb1  10887  supxrunb2  10888  ixxin  10922  difreicc  11017  iccsplit  11018  iccshftr  11019  iccshftl  11021  iccdil  11023  icccntr  11025  fzaddel  11076  fzrev  11097  modadd1  11266  modmul1  11267  mulexp  11407  expadd  11410  expmul  11413  leexp1a  11426  expnbnd  11496  bccl  11601  hashdom  11641  hashfacen  11691  revccat  11786  2shfti  11883  cau3lem  12146  subcn2  12376  caucvgb  12461  iseraltlem1  12463  sumss  12506  incexclem  12604  supcvg  12623  mertenslem2  12650  eftlcl  12696  reeftlcl  12697  rpnnen2lem6  12807  dvdsext  12888  3dvds  12900  gcdcllem3  13001  seq1st  13050  dvdsprime  13080  pc2dvds  13240  prmpwdvds  13260  unbenlem  13264  infpnlem1  13266  1arith  13283  vdwmc2  13335  ramcl  13385  mrcuni  13834  isacs1i  13870  acsfn  13872  funcpropd  14085  natpropd  14161  curfcl  14317  curf2ndf  14332  spwpr2  14648  resmhm  14747  resmhm2b  14749  mhmco  14750  mhmima  14751  pwsdiagmhm  14756  gsumwsubmcl  14772  gsumwspan  14779  subgint  14952  ghmmhmb  15005  resghm  15010  cntzmhm  15125  dfod2  15188  gexdvds  15206  subgpgp  15219  sylow1lem3  15222  frgpnabllem1  15472  dprdfeq0  15568  isdrng2  15833  cntzsubr  15888  islmodd  15944  lsslss  16025  reslmhm2b  16118  psrbaglefi  16425  ply1coe  16672  ocvocv  16886  elcls  17125  leordtval  17265  cnpnei  17316  cnco  17318  cnss1  17328  cmpsub  17451  hauscmplem  17457  ptbasid  17595  tx2cn  17630  upxp  17643  txindis  17654  xkoptsub  17674  xkopt  17675  trfbas2  17863  filcon  17903  trfil2  17907  filssufilg  17931  ufileu  17939  fixufil  17942  ufilen  17950  rnelfmlem  17972  flimclsi  17998  hauspwpwf1  18007  fclsopn  18034  fclsfnflim  18047  fclscmpi  18049  alexsubALTlem3  18068  alexsubALTlem4  18069  ptcmplem5  18075  tgpmulg  18111  subgtgp  18123  tgpt0  18136  tsmsxplem2  18171  metss  18526  metustfbasOLD  18583  metustfbas  18584  dscopn  18609  xrsmopn  18831  cncfss  18917  icoopnst  18952  iccpnfcnv  18957  icccvx  18963  evth  18972  phtpycc  19004  pcohtpylem  19032  lmmbrf  19203  fgcfil  19212  caucfil  19224  cfilres  19237  bcth3  19272  ovolfioo  19352  ovolficc  19353  voliunlem3  19434  volcn  19486  mbflimsup  19546  mbfi1fseqlem5  19599  itg2seq  19622  dvnff  19797  dvnadd  19803  cpnord  19809  c1liplem1  19868  plypf1  20119  plyaddlem1  20120  plymullem1  20121  coeeulem  20131  coeidlem  20144  dgrle  20150  plycjlem  20182  elqaalem3  20226  ulmcaulem  20298  ulmcau  20299  psergf  20316  psercn2  20327  efopn  20537  abscxpbnd  20625  leibpi  20770  isppw2  20886  muinv  20966  bposlem3  21058  pntrmax  21246  pntpbnd1  21268  qabvexp  21308  usgraidx2vlem2  21399  cusgrares  21469  cusgrafilem2  21477  eupath2lem3  21689  grpoidinvlem3  21782  grpoidinv  21784  grpoideu  21785  subgoablo  21887  nmoub3i  22262  nmlno0lem  22282  nmlnoubi  22285  ipasslem3  22322  ipblnfi  22345  hvaddsub4  22568  his35  22578  shsel3  22805  chj4  23025  spansncol  23058  chscllem2  23128  5oalem2  23145  3oalem2  23153  hoaddcl  23249  adjsym  23324  cnvadj  23383  hhcno  23395  hhcnf  23396  nmopub2tALT  23400  unoplin  23411  counop  23412  nmfnleub2  23417  hmoplin  23433  brafnmul  23442  nmlnop0iALT  23486  nmopun  23505  nmophmi  23522  riesz3i  23553  riesz1  23556  cnlnadjlem2  23559  cnlnadjlem6  23563  adjmul  23583  adjadd  23584  bra11  23599  cnvbraval  23601  kbass5  23611  kbass6  23612  leop2  23615  leopadd  23623  leopmuli  23624  leoptri  23627  leopnmid  23629  nmopleid  23630  pj3si  23698  hstel2  23710  cvcon3  23775  dmdmd  23791  dmdbr5  23799  mdsl0  23801  mdslmd1lem1  23816  mdslmd1lem2  23817  mdslmd3i  23823  superpos  23845  chirredlem2  23882  chirredlem3  23883  mdsymlem3  23896  mdsymlem5  23898  mdsymlem6  23899  sumdmdlem  23909  cdjreui  23923  cdj1i  23924  cdj3i  23932  abfmpel  24055  fcomptf  24065  xrge0iifcnv  24307  esumcst  24443  hasheuni  24463  sigaclcu2  24491  insiga  24508  measres  24564  measdivcst  24567  volfiniune  24574  sconpi1  24914  cvmsss2  24949  fprodn0  25292  dfon2lem6  25399  predpo  25439  preddowncl  25451  dftrpred3g  25491  poseq  25508  soseq  25509  nodenselem3  25592  nobndlem6  25606  eqeelen  25791  colinearalglem4  25796  axcgrid  25803  axsegconlem1  25804  axsegconlem3  25806  ax5seglem1  25815  ax5seglem2  25816  ax5seglem9  25824  axcontlem2  25852  hfext  26072  mblfinlem  26190  mblfinlem2  26191  mblfinlem3  26192  ex-ovoliunnfl  26195  mbfresfi  26199  cnambfre  26201  itg2addnclem  26202  itg2addnclem2  26203  itg2addnc  26205  bddiblnc  26221  elicc3  26257  fnessref  26310  eqfnun  26360  indexdom  26373  filbcmb  26379  fzadd2  26382  fdc  26386  incsequz  26389  metf1o  26398  caures  26403  bndss  26432  ismtycnv  26448  heiborlem1  26457  rrncmslem  26478  isdrngo2  26511  rngoisocnv  26534  unichnidl  26578  nacsfix  26703  eq0rabdioph  26772  diophren  26811  rencldnfilem  26818  pell1234qrdich  26861  jm2.24  26965  bezoutr1  26988  jm2.26lem3  27009  wepwsolem  27053  pwssplit4  27106  frlmsslsp  27163  frlmlbs  27164  isnumbasgrplem3  27185  dgrnznn  27255  f1omvdconj  27304  mamudi  27376  mamudir  27377  ofsubid  27456  stirlinglem5  27741  2f1fvneq  28008  shwrdidx  28130  2shwrd2lem1  28142  lswrdn0  28149  usgra2pthlem1  28184  el2wlkonot  28210  el2spthonot0  28212  frgrancvvdeqlemB  28285  frgrawopreglem5  28295  frghash2spot  28310  lshpset2N  29756  pmapglb2N  30407  pmapglb2xN  30408  pclfinN  30536  polval2N  30542  cdleme31fv2  31029  cdleme32fvcl  31076  cdleme48gfv  31173  tendoicl  31432  tendoipl  31433  diaglbN  31692  dochkr1  32115  dochkr1OLDN  32116
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