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

Theorem adantll 694
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 447 . 2  |-  ( ( th  /\  ph )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 457 1  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  ad2antlr  707  ad2ant2l  726  ad2ant2lr  728  3ad2antl3  1119  3adant1l  1174  ax11eq  2145  ax11el  2146  nfeud2  2168  ralcom2  2717  reu6  2967  sbc2iegf  3070  sbcralt  3076  pofun  4346  tz7.7  4434  onfr  4447  limsssuc  4657  poinxp  4769  sossfld  5136  ssimaex  5600  fndmdif  5645  dffo4  5692  foco2  5696  fcompt  5710  fconst2g  5744  isores3  5848  curry1  6226  curry2  6229  onnseq  6377  oe0  6537  oesuclem  6540  oecl  6552  oaordi  6560  oawordri  6564  oaass  6575  omordi  6580  omword2  6588  omlimcl  6592  odi  6593  omass  6594  oeoe  6613  nnaordi  6632  oaabs  6658  omsmolem  6667  eceqoveq  6779  dom2lem  6917  sbthlem9  6995  php3  7063  onomeneq  7066  isinf  7092  frfi  7118  fiint  7149  fodomfib  7152  fofinf1o  7153  marypha1lem  7202  ordiso2  7246  unwdomg  7314  xpwdomg  7315  ac5num  7679  cff1  7900  cfcoflem  7914  infpssrlem4  7948  isf32lem9  8003  isf34lem7  8021  fin1a2lem13  8054  fin1a2s  8056  hsmexlem4  8071  axdc2lem  8090  zorn2lem6  8144  inttsk  8412  tskuni  8421  nqereu  8569  prcdnq  8633  addclprlem2  8657  ltexpri  8683  prlem936  8687  reclem2pr  8688  axsup  8914  add4  9043  ltleadd  9273  lt2mul2div  9648  lediv12a  9665  infmrcl  9749  nn2ge  9787  zextle  10101  fnn0ind  10127  xrlttr  10490  ifle  10540  xaddass  10585  xmulasslem3  10622  xlemul1a  10624  xadddilem  10630  xrsupsslem  10641  xrinfmsslem  10642  supxrunb1  10654  supxrunb2  10655  ixxin  10689  difreicc  10783  iccsplit  10784  iccshftr  10785  iccshftl  10787  iccdil  10789  icccntr  10791  fzaddel  10842  fzrev  10862  modadd1  11017  modmul1  11018  mulexp  11157  expadd  11160  expmul  11163  leexp1a  11176  expnbnd  11246  bccl  11350  hashdom  11377  hashfacen  11408  revccat  11500  2shfti  11591  cau3lem  11854  subcn2  12084  caucvgb  12168  iseraltlem1  12170  sumss  12213  incexclem  12311  supcvg  12330  mertenslem2  12357  eftlcl  12403  reeftlcl  12404  rpnnen2lem6  12514  dvdsext  12595  3dvds  12607  gcdcllem3  12708  seq1st  12757  dvdsprime  12787  pc2dvds  12947  prmpwdvds  12967  unbenlem  12971  infpnlem1  12973  1arith  12990  vdwmc2  13042  ramcl  13092  mrcuni  13539  isacs1i  13575  acsfn  13577  funcpropd  13790  natpropd  13866  curfcl  14022  curf2ndf  14037  spwpr2  14353  resmhm  14452  resmhm2b  14454  mhmco  14455  mhmima  14456  pwsdiagmhm  14461  gsumwsubmcl  14477  gsumwspan  14484  subgint  14657  ghmmhmb  14710  resghm  14715  cntzmhm  14830  dfod2  14893  gexdvds  14911  subgpgp  14924  sylow1lem3  14927  frgpnabllem1  15177  dprdfeq0  15273  isdrng2  15538  cntzsubr  15593  islmodd  15649  lsslss  15734  reslmhm2b  15827  psrbaglefi  16134  ply1coe  16384  ocvocv  16587  elcls  16826  leordtval  16959  cnpnei  17009  cnco  17011  cnss1  17021  cmpsub  17143  hauscmplem  17149  ptbasid  17286  tx2cn  17320  upxp  17333  txindis  17344  xkoptsub  17364  xkopt  17365  trfbas2  17554  filcon  17594  trfil2  17598  filssufilg  17622  ufileu  17630  fixufil  17633  ufilen  17641  rnelfmlem  17663  flimclsi  17689  hauspwpwf1  17698  fclsopn  17725  fclsfnflim  17738  fclscmpi  17740  alexsubALTlem3  17759  alexsubALTlem4  17760  ptcmplem5  17766  tgpmulg  17792  subgtgp  17804  tgpt0  17817  tsmsxplem2  17852  metss  18070  dscopn  18112  xrsmopn  18334  cncfss  18419  icoopnst  18453  iccpnfcnv  18458  icccvx  18464  evth  18473  phtpycc  18505  pcohtpylem  18533  lmmbrf  18704  fgcfil  18713  caucfil  18725  cfilres  18738  bcth3  18769  ovolfioo  18843  ovolficc  18844  voliunlem3  18925  volcn  18977  mbflimsup  19037  mbfi1fseqlem5  19090  itg2seq  19113  dvnff  19288  dvnadd  19294  cpnord  19300  c1liplem1  19359  plypf1  19610  plyaddlem1  19611  plymullem1  19612  coeeulem  19622  coeidlem  19635  dgrle  19641  plycjlem  19673  elqaalem3  19717  ulmcaulem  19787  ulmcau  19788  psergf  19804  psercn2  19815  efopn  20021  abscxpbnd  20109  leibpi  20254  isppw2  20369  muinv  20449  bposlem3  20541  pntrmax  20729  pntpbnd1  20751  qabvexp  20791  grpoidinvlem3  20889  grpoidinv  20891  grpoideu  20892  subgoablo  20994  nmoub3i  21367  nmlno0lem  21387  nmlnoubi  21390  ipasslem3  21427  ipblnfi  21450  hvaddsub4  21673  his35  21683  shsel3  21910  chj4  22130  spansncol  22163  chscllem2  22233  5oalem2  22250  3oalem2  22258  hoaddcl  22354  adjsym  22429  cnvadj  22488  hhcno  22500  hhcnf  22501  nmopub2tALT  22505  unoplin  22516  counop  22517  nmfnleub2  22522  hmoplin  22538  brafnmul  22547  nmlnop0iALT  22591  nmopun  22610  nmophmi  22627  riesz3i  22658  riesz1  22661  cnlnadjlem2  22664  cnlnadjlem6  22668  adjmul  22688  adjadd  22689  bra11  22704  cnvbraval  22706  kbass5  22716  kbass6  22717  leop2  22720  leopadd  22728  leopmuli  22729  leoptri  22732  leopnmid  22734  nmopleid  22735  pj3si  22803  hstel2  22815  cvcon3  22880  dmdmd  22896  dmdbr5  22904  mdsl0  22906  mdslmd1lem1  22921  mdslmd1lem2  22922  mdslmd3i  22928  superpos  22950  chirredlem2  22987  chirredlem3  22988  mdsymlem3  23001  mdsymlem5  23003  mdsymlem6  23004  sumdmdlem  23014  cdjreui  23028  cdj1i  23029  cdj3i  23037  fcomptf  23245  xrge0iifcnv  23330  hasheuni  23468  sigaclcu2  23496  insiga  23513  sconpi1  23785  cvmsss2  23820  eupath2lem3  23918  dfon2lem6  24215  predpo  24255  preddowncl  24267  dftrpred3g  24307  poseq  24324  soseq  24325  nodenselem3  24408  nobndlem6  24422  eqeelen  24604  colinearalglem4  24609  axcgrid  24616  axsegconlem1  24617  axsegconlem3  24619  ax5seglem1  24628  ax5seglem2  24629  ax5seglem9  24637  axcontlem2  24665  hfext  24885  ex-ovoliunnfl  25002  itg2addnclem2  25004  itg2addnc  25005  bddiblnc  25021  surjsec2  25223  toplat  25393  ltrcmp  25508  supexr  25734  idsubfun  25961  elicc3  26331  fnessref  26396  eqfnun  26490  indexdom  26516  filbcmb  26535  fzadd2  26547  fdc  26558  incsequz  26561  metf1o  26572  caures  26579  bndss  26613  ismtycnv  26629  heiborlem1  26638  rrncmslem  26659  isdrngo2  26692  rngoisocnv  26715  unichnidl  26759  nacsfix  26890  eq0rabdioph  26959  diophren  26999  rencldnfilem  27006  pell1234qrdich  27049  jm2.24  27153  bezoutr1  27176  jm2.26lem3  27197  wepwsolem  27241  pwssplit4  27294  frlmsslsp  27351  frlmlbs  27352  isnumbasgrplem3  27373  dgrnznn  27443  f1omvdconj  27492  mamudi  27564  mamudir  27565  ofsubid  27644  stirlinglem5  27930  lshpset2N  29931  pmapglb2N  30582  pmapglb2xN  30583  pclfinN  30711  polval2N  30717  cdleme31fv2  31204  cdleme32fvcl  31251  cdleme48gfv  31348  tendoicl  31607  tendoipl  31608  diaglbN  31867  dochkr1  32290  dochkr1OLDN  32291
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 177  df-an 360
  Copyright terms: Public domain W3C validator