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  2243  ax11el  2244  nfeud2  2266  ralcom2  2832  reu6  3083  sbc2iegf  3187  sbcralt  3193  pofun  4479  tz7.7  4567  onfr  4580  limsssuc  4789  poinxp  4900  sossfld  5276  ssimaex  5747  fndmdif  5793  dffo4  5844  foco2  5848  fcompt  5863  fconst2g  5905  isores3  6014  curry1  6397  curry2  6400  onnseq  6565  oe0  6725  oesuclem  6728  oecl  6740  oaordi  6748  oawordri  6752  oaass  6763  omordi  6768  omword2  6776  omlimcl  6780  odi  6781  omass  6782  oeoe  6801  nnaordi  6820  oaabs  6846  omsmolem  6855  eceqoveq  6968  dom2lem  7106  sbthlem9  7184  php3  7252  onomeneq  7255  isinf  7281  frfi  7311  fiint  7342  fodomfib  7345  fofinf1o  7346  marypha1lem  7396  ordiso2  7440  unwdomg  7508  xpwdomg  7509  ac5num  7873  cff1  8094  cfcoflem  8108  infpssrlem4  8142  isf32lem9  8197  isf34lem7  8215  fin1a2lem13  8248  fin1a2s  8250  hsmexlem4  8265  axdc2lem  8284  zorn2lem6  8337  inttsk  8605  tskuni  8614  nqereu  8762  prcdnq  8826  addclprlem2  8850  ltexpri  8876  prlem936  8880  reclem2pr  8881  axsup  9107  add4  9237  ltleadd  9467  lt2mul2div  9842  lediv12a  9859  infmrcl  9943  nn2ge  9981  zextle  10299  fnn0ind  10325  xrlttr  10689  ifle  10739  xaddass  10784  xmulasslem3  10821  xlemul1a  10823  xadddilem  10829  xrsupsslem  10841  xrinfmsslem  10842  supxrunb1  10854  supxrunb2  10855  ixxin  10889  difreicc  10984  iccsplit  10985  iccshftr  10986  iccshftl  10988  iccdil  10990  icccntr  10992  fzaddel  11043  fzrev  11064  modadd1  11233  modmul1  11234  mulexp  11374  expadd  11377  expmul  11380  leexp1a  11393  expnbnd  11463  bccl  11568  hashdom  11608  hashfacen  11658  revccat  11753  2shfti  11850  cau3lem  12113  subcn2  12343  caucvgb  12428  iseraltlem1  12430  sumss  12473  incexclem  12571  supcvg  12590  mertenslem2  12617  eftlcl  12663  reeftlcl  12664  rpnnen2lem6  12774  dvdsext  12855  3dvds  12867  gcdcllem3  12968  seq1st  13017  dvdsprime  13047  pc2dvds  13207  prmpwdvds  13227  unbenlem  13231  infpnlem1  13233  1arith  13250  vdwmc2  13302  ramcl  13352  mrcuni  13801  isacs1i  13837  acsfn  13839  funcpropd  14052  natpropd  14128  curfcl  14284  curf2ndf  14299  spwpr2  14615  resmhm  14714  resmhm2b  14716  mhmco  14717  mhmima  14718  pwsdiagmhm  14723  gsumwsubmcl  14739  gsumwspan  14746  subgint  14919  ghmmhmb  14972  resghm  14977  cntzmhm  15092  dfod2  15155  gexdvds  15173  subgpgp  15186  sylow1lem3  15189  frgpnabllem1  15439  dprdfeq0  15535  isdrng2  15800  cntzsubr  15855  islmodd  15911  lsslss  15992  reslmhm2b  16085  psrbaglefi  16392  ply1coe  16639  ocvocv  16853  elcls  17092  leordtval  17231  cnpnei  17282  cnco  17284  cnss1  17294  cmpsub  17417  hauscmplem  17423  ptbasid  17560  tx2cn  17595  upxp  17608  txindis  17619  xkoptsub  17639  xkopt  17640  trfbas2  17828  filcon  17868  trfil2  17872  filssufilg  17896  ufileu  17904  fixufil  17907  ufilen  17915  rnelfmlem  17937  flimclsi  17963  hauspwpwf1  17972  fclsopn  17999  fclsfnflim  18012  fclscmpi  18014  alexsubALTlem3  18033  alexsubALTlem4  18034  ptcmplem5  18040  tgpmulg  18076  subgtgp  18088  tgpt0  18101  tsmsxplem2  18136  metss  18491  metustfbasOLD  18548  metustfbas  18549  dscopn  18574  xrsmopn  18796  cncfss  18882  icoopnst  18917  iccpnfcnv  18922  icccvx  18928  evth  18937  phtpycc  18969  pcohtpylem  18997  lmmbrf  19168  fgcfil  19177  caucfil  19189  cfilres  19202  bcth3  19237  ovolfioo  19317  ovolficc  19318  voliunlem3  19399  volcn  19451  mbflimsup  19511  mbfi1fseqlem5  19564  itg2seq  19587  dvnff  19762  dvnadd  19768  cpnord  19774  c1liplem1  19833  plypf1  20084  plyaddlem1  20085  plymullem1  20086  coeeulem  20096  coeidlem  20109  dgrle  20115  plycjlem  20147  elqaalem3  20191  ulmcaulem  20263  ulmcau  20264  psergf  20281  psercn2  20292  efopn  20502  abscxpbnd  20590  leibpi  20735  isppw2  20851  muinv  20931  bposlem3  21023  pntrmax  21211  pntpbnd1  21233  qabvexp  21273  usgraidx2vlem2  21364  cusgrares  21434  cusgrafilem2  21442  eupath2lem3  21654  grpoidinvlem3  21747  grpoidinv  21749  grpoideu  21750  subgoablo  21852  nmoub3i  22227  nmlno0lem  22247  nmlnoubi  22250  ipasslem3  22287  ipblnfi  22310  hvaddsub4  22533  his35  22543  shsel3  22770  chj4  22990  spansncol  23023  chscllem2  23093  5oalem2  23110  3oalem2  23118  hoaddcl  23214  adjsym  23289  cnvadj  23348  hhcno  23360  hhcnf  23361  nmopub2tALT  23365  unoplin  23376  counop  23377  nmfnleub2  23382  hmoplin  23398  brafnmul  23407  nmlnop0iALT  23451  nmopun  23470  nmophmi  23487  riesz3i  23518  riesz1  23521  cnlnadjlem2  23524  cnlnadjlem6  23528  adjmul  23548  adjadd  23549  bra11  23564  cnvbraval  23566  kbass5  23576  kbass6  23577  leop2  23580  leopadd  23588  leopmuli  23589  leoptri  23592  leopnmid  23594  nmopleid  23595  pj3si  23663  hstel2  23675  cvcon3  23740  dmdmd  23756  dmdbr5  23764  mdsl0  23766  mdslmd1lem1  23781  mdslmd1lem2  23782  mdslmd3i  23788  superpos  23810  chirredlem2  23847  chirredlem3  23848  mdsymlem3  23861  mdsymlem5  23863  mdsymlem6  23864  sumdmdlem  23874  cdjreui  23888  cdj1i  23889  cdj3i  23897  abfmpel  24020  fcomptf  24030  xrge0iifcnv  24272  esumcst  24408  hasheuni  24428  sigaclcu2  24456  insiga  24473  measres  24529  measdivcst  24532  volfiniune  24539  sconpi1  24879  cvmsss2  24914  fprodn0  25256  dfon2lem6  25358  predpo  25398  preddowncl  25410  dftrpred3g  25450  poseq  25467  soseq  25468  nodenselem3  25551  nobndlem6  25565  eqeelen  25747  colinearalglem4  25752  axcgrid  25759  axsegconlem1  25760  axsegconlem3  25762  ax5seglem1  25771  ax5seglem2  25772  ax5seglem9  25780  axcontlem2  25808  hfext  26028  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ex-ovoliunnfl  26148  mbfresfi  26152  cnambfre  26154  itg2addnclem  26155  itg2addnclem2  26156  itg2addnc  26158  bddiblnc  26174  elicc3  26210  fnessref  26263  eqfnun  26313  indexdom  26326  filbcmb  26332  fzadd2  26335  fdc  26339  incsequz  26342  metf1o  26351  caures  26356  bndss  26385  ismtycnv  26401  heiborlem1  26410  rrncmslem  26431  isdrngo2  26464  rngoisocnv  26487  unichnidl  26531  nacsfix  26656  eq0rabdioph  26725  diophren  26764  rencldnfilem  26771  pell1234qrdich  26814  jm2.24  26918  bezoutr1  26941  jm2.26lem3  26962  wepwsolem  27006  pwssplit4  27059  frlmsslsp  27116  frlmlbs  27117  isnumbasgrplem3  27138  dgrnznn  27208  f1omvdconj  27257  mamudi  27329  mamudir  27330  ofsubid  27409  stirlinglem5  27694  2f1fvneq  27958  usgra2pthlem1  28040  el2wlkonot  28066  el2spthonot0  28068  frgrancvvdeqlemB  28141  frgrawopreglem5  28151  frghash2spot  28166  lshpset2N  29602  pmapglb2N  30253  pmapglb2xN  30254  pclfinN  30382  polval2N  30388  cdleme31fv2  30875  cdleme32fvcl  30922  cdleme48gfv  31019  tendoicl  31278  tendoipl  31279  diaglbN  31538  dochkr1  31961  dochkr1OLDN  31962
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