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  2132  ax11el  2133  nfeud2  2155  ralcom2  2704  reu6  2954  sbc2iegf  3057  sbcralt  3063  pofun  4330  tz7.7  4418  onfr  4431  limsssuc  4641  poinxp  4753  sossfld  5120  ssimaex  5584  fndmdif  5629  dffo4  5676  foco2  5680  fcompt  5694  fconst2g  5728  isores3  5832  curry1  6210  curry2  6213  onnseq  6361  oe0  6521  oesuclem  6524  oecl  6536  oaordi  6544  oawordri  6548  oaass  6559  omordi  6564  omword2  6572  omlimcl  6576  odi  6577  omass  6578  oeoe  6597  nnaordi  6616  oaabs  6642  omsmolem  6651  eceqoveq  6763  dom2lem  6901  sbthlem9  6979  php3  7047  onomeneq  7050  isinf  7076  frfi  7102  fiint  7133  fodomfib  7136  fofinf1o  7137  marypha1lem  7186  ordiso2  7230  unwdomg  7298  xpwdomg  7299  ac5num  7663  cff1  7884  cfcoflem  7898  infpssrlem4  7932  isf32lem9  7987  isf34lem7  8005  fin1a2lem13  8038  fin1a2s  8040  hsmexlem4  8055  axdc2lem  8074  zorn2lem6  8128  inttsk  8396  tskuni  8405  nqereu  8553  prcdnq  8617  addclprlem2  8641  ltexpri  8667  prlem936  8671  reclem2pr  8672  axsup  8898  add4  9027  ltleadd  9257  lt2mul2div  9632  lediv12a  9649  infmrcl  9733  nn2ge  9771  zextle  10085  fnn0ind  10111  xrlttr  10474  ifle  10524  xaddass  10569  xmulasslem3  10606  xlemul1a  10608  xadddilem  10614  xrsupsslem  10625  xrinfmsslem  10626  supxrunb1  10638  supxrunb2  10639  ixxin  10673  difreicc  10767  iccsplit  10768  iccshftr  10769  iccshftl  10771  iccdil  10773  icccntr  10775  fzaddel  10826  fzrev  10846  modadd1  11001  modmul1  11002  mulexp  11141  expadd  11144  expmul  11147  leexp1a  11160  expnbnd  11230  bccl  11334  hashdom  11361  hashfacen  11392  revccat  11484  2shfti  11575  cau3lem  11838  subcn2  12068  caucvgb  12152  iseraltlem1  12154  sumss  12197  incexclem  12295  supcvg  12314  mertenslem2  12341  eftlcl  12387  reeftlcl  12388  rpnnen2lem6  12498  dvdsext  12579  3dvds  12591  gcdcllem3  12692  seq1st  12741  dvdsprime  12771  pc2dvds  12931  prmpwdvds  12951  unbenlem  12955  infpnlem1  12957  1arith  12974  vdwmc2  13026  ramcl  13076  mrcuni  13523  isacs1i  13559  acsfn  13561  funcpropd  13774  natpropd  13850  curfcl  14006  curf2ndf  14021  spwpr2  14337  resmhm  14436  resmhm2b  14438  mhmco  14439  mhmima  14440  pwsdiagmhm  14445  gsumwsubmcl  14461  gsumwspan  14468  subgint  14641  ghmmhmb  14694  resghm  14699  cntzmhm  14814  dfod2  14877  gexdvds  14895  subgpgp  14908  sylow1lem3  14911  frgpnabllem1  15161  dprdfeq0  15257  isdrng2  15522  cntzsubr  15577  islmodd  15633  lsslss  15718  reslmhm2b  15811  psrbaglefi  16118  ply1coe  16368  ocvocv  16571  elcls  16810  leordtval  16943  cnpnei  16993  cnco  16995  cnss1  17005  cmpsub  17127  hauscmplem  17133  ptbasid  17270  tx2cn  17304  upxp  17317  txindis  17328  xkoptsub  17348  xkopt  17349  trfbas2  17538  filcon  17578  trfil2  17582  filssufilg  17606  ufileu  17614  fixufil  17617  ufilen  17625  rnelfmlem  17647  flimclsi  17673  hauspwpwf1  17682  fclsopn  17709  fclsfnflim  17722  fclscmpi  17724  alexsubALTlem3  17743  alexsubALTlem4  17744  ptcmplem5  17750  tgpmulg  17776  subgtgp  17788  tgpt0  17801  tsmsxplem2  17836  metss  18054  dscopn  18096  xrsmopn  18318  cncfss  18403  icoopnst  18437  iccpnfcnv  18442  icccvx  18448  evth  18457  phtpycc  18489  pcohtpylem  18517  lmmbrf  18688  fgcfil  18697  caucfil  18709  cfilres  18722  bcth3  18753  ovolfioo  18827  ovolficc  18828  voliunlem3  18909  volcn  18961  mbflimsup  19021  mbfi1fseqlem5  19074  itg2seq  19097  dvnff  19272  dvnadd  19278  cpnord  19284  c1liplem1  19343  plypf1  19594  plyaddlem1  19595  plymullem1  19596  coeeulem  19606  coeidlem  19619  dgrle  19625  plycjlem  19657  elqaalem3  19701  ulmcaulem  19771  ulmcau  19772  psergf  19788  psercn2  19799  efopn  20005  abscxpbnd  20093  leibpi  20238  isppw2  20353  muinv  20433  bposlem3  20525  pntrmax  20713  pntpbnd1  20735  qabvexp  20775  grpoidinvlem3  20873  grpoidinv  20875  grpoideu  20876  subgoablo  20978  nmoub3i  21351  nmlno0lem  21371  nmlnoubi  21374  ipasslem3  21411  ipblnfi  21434  hvaddsub4  21657  his35  21667  shsel3  21894  chj4  22114  spansncol  22147  chscllem2  22217  5oalem2  22234  3oalem2  22242  hoaddcl  22338  adjsym  22413  cnvadj  22472  hhcno  22484  hhcnf  22485  nmopub2tALT  22489  unoplin  22500  counop  22501  nmfnleub2  22506  hmoplin  22522  brafnmul  22531  nmlnop0iALT  22575  nmopun  22594  nmophmi  22611  riesz3i  22642  riesz1  22645  cnlnadjlem2  22648  cnlnadjlem6  22652  adjmul  22672  adjadd  22673  bra11  22688  cnvbraval  22690  kbass5  22700  kbass6  22701  leop2  22704  leopadd  22712  leopmuli  22713  leoptri  22716  leopnmid  22718  nmopleid  22719  pj3si  22787  hstel2  22799  cvcon3  22864  dmdmd  22880  dmdbr5  22888  mdsl0  22890  mdslmd1lem1  22905  mdslmd1lem2  22906  mdslmd3i  22912  superpos  22934  chirredlem2  22971  chirredlem3  22972  mdsymlem3  22985  mdsymlem5  22987  mdsymlem6  22988  sumdmdlem  22998  cdjreui  23012  cdj1i  23013  cdj3i  23021  fcomptf  23230  xrge0iifcnv  23315  hasheuni  23453  sigaclcu2  23481  insiga  23498  sconpi1  23770  cvmsss2  23805  eupath2lem3  23903  dfon2lem6  24144  predpo  24184  preddowncl  24196  dftrpred3g  24236  poseq  24253  soseq  24254  nodenselem3  24337  nobndlem6  24351  eqeelen  24532  colinearalglem4  24537  axcgrid  24544  axsegconlem1  24545  axsegconlem3  24547  ax5seglem1  24556  ax5seglem2  24557  ax5seglem9  24565  axcontlem2  24593  hfext  24813  surjsec2  25120  toplat  25290  ltrcmp  25405  supexr  25631  idsubfun  25858  elicc3  26228  fnessref  26293  eqfnun  26387  indexdom  26413  filbcmb  26432  fzadd2  26444  fdc  26455  incsequz  26458  metf1o  26469  caures  26476  bndss  26510  ismtycnv  26526  heiborlem1  26535  rrncmslem  26556  isdrngo2  26589  rngoisocnv  26612  unichnidl  26656  nacsfix  26787  eq0rabdioph  26856  diophren  26896  rencldnfilem  26903  pell1234qrdich  26946  jm2.24  27050  bezoutr1  27073  jm2.26lem3  27094  wepwsolem  27138  pwssplit4  27191  frlmsslsp  27248  frlmlbs  27249  isnumbasgrplem3  27270  dgrnznn  27340  f1omvdconj  27389  mamudi  27461  mamudir  27462  ofsubid  27541  stirlinglem5  27827  lshpset2N  29309  pmapglb2N  29960  pmapglb2xN  29961  pclfinN  30089  polval2N  30095  cdleme31fv2  30582  cdleme32fvcl  30629  cdleme48gfv  30726  tendoicl  30985  tendoipl  30986  diaglbN  31245  dochkr1  31668  dochkr1OLDN  31669
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