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

Theorem adantll 713
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 461 . 2  |-  ( ( th  /\  ph )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 471 1  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  ad2antlr  726  ad2ant2l  745  ad2ant2lr  747  3ad2antl3  1152  3adant1l  1210  ax12eq  2241  ax12el  2242  nfeud2OLD  2278  ralcom2  2880  reu6  3143  sbc2iegf  3256  sbcralt  3262  pofun  4652  tz7.7  4740  onfr  4753  poinxp  4897  xpdifid  5261  sossfld  5280  ssimaex  5751  fndmdif  5802  dffo4  5854  foco2  5858  fcompt  5874  fconst2g  5927  isores3  6021  limsssuc  6456  curry1  6659  curry2  6662  extmptsuppeq  6708  suppss  6714  suppssov1  6716  suppss2  6718  suppssfv  6720  onnseq  6797  oe0  6954  oesuclem  6957  oecl  6969  oaordi  6977  oawordri  6981  oaass  6992  omordi  6997  omword2  7005  omlimcl  7009  odi  7010  omass  7011  oeoe  7030  nnaordi  7049  oaabs  7075  omsmolem  7084  eceqoveq  7197  dom2lem  7341  sbthlem9  7421  php3  7489  onomeneq  7492  isinf  7518  frfi  7549  fiint  7580  fodomfib  7583  fofinf1o  7584  marypha1lem  7675  ordiso2  7721  unwdomg  7791  xpwdomg  7792  ac5num  8198  cff1  8419  cfcoflem  8433  infpssrlem4  8467  isf32lem9  8522  isf34lem7  8540  fin1a2lem13  8573  fin1a2s  8575  hsmexlem4  8590  axdc2lem  8609  zorn2lem6  8662  axpowndlem2  8754  inttsk  8933  tskuni  8942  nqereu  9090  prcdnq  9154  addclprlem2  9178  ltexpri  9204  prlem936  9208  reclem2pr  9209  axsup  9442  add4  9577  ltleadd  9814  lt2mul2div  10200  lediv12a  10217  infmrcl  10301  nn2ge  10339  zextle  10707  fnn0ind  10733  xrlttr  11109  ifle  11159  xaddass  11204  xmulasslem3  11241  xlemul1a  11243  xadddilem  11249  xrsupsslem  11261  xrinfmsslem  11262  supxrunb1  11274  supxrunb2  11275  ixxin  11309  difreicc  11409  iccsplit  11410  iccshftr  11411  iccshftl  11413  iccdil  11415  icccntr  11417  fzaddel  11485  fzrev  11511  modadd1  11737  modmul1  11744  mulexp  11895  expadd  11898  expmul  11901  leexp1a  11914  expnbnd  11985  bccl  12090  hashdom  12134  hashfacen  12199  swrdccat3blem  12378  revccat  12398  2shfti  12561  cau3lem  12834  subcn2  13064  caucvgb  13149  iseraltlem1  13151  sumss  13193  incexclem  13291  supcvg  13310  mertenslem2  13337  eftlcl  13383  reeftlcl  13384  rpnnen2lem6  13494  dvdsext  13576  3dvds  13588  gcdcllem3  13689  seq1st  13738  dvdsprime  13768  pc2dvds  13937  prmpwdvds  13957  unbenlem  13961  infpnlem1  13963  1arith  13980  vdwmc2  14032  ramcl  14082  mrcuni  14551  isacs1i  14587  acsfn  14589  funcpropd  14802  natpropd  14878  curfcl  15034  curf2ndf  15049  resmhm  15478  resmhm2b  15480  mhmco  15481  mhmima  15482  pwsdiagmhm  15488  gsumwsubmcl  15507  gsumwspan  15515  grpissubg  15692  subgint  15696  ghmmhmb  15749  resghm  15754  cntzmhm  15847  symgextf1lem  15916  f1omvdconj  15943  pmtr3ncom  15972  dfod2  16056  gexdvds  16074  subgpgp  16087  sylow1lem3  16090  frgpnabllem1  16342  dprdfeq0  16500  dprdfeq0OLD  16507  isdrng2  16820  cntzsubr  16875  islmodd  16932  lsslss  17019  reslmhm2b  17112  psrbaglefi  17418  psrbaglefiOLD  17419  ply1coe  17721  ply1coeOLD  17722  psgnfix1  18003  psgndif  18007  zrhcopsgndif  18008  ocvocv  18071  frlmsslsp  18198  frlmsslspOLD  18199  frlmlbs  18200  mamudi  18282  mamudir  18283  mulmarep1gsum2  18360  mdetunilem7  18399  mdetunilem9  18401  gsummatr01lem3  18438  smadiadetlem3  18449  elcls  18652  leordtval  18792  cnpnei  18843  cnco  18845  cnss1  18855  cmpsub  18978  hauscmplem  18984  ptbasid  19123  tx2cn  19158  upxp  19171  txindis  19182  xkoptsub  19202  xkopt  19203  trfbas2  19391  filcon  19431  trfil2  19435  filssufilg  19459  ufileu  19467  fixufil  19470  ufilen  19478  rnelfmlem  19500  flimclsi  19526  hauspwpwf1  19535  fclsopn  19562  fclsfnflim  19575  fclscmpi  19577  alexsubALTlem3  19596  alexsubALTlem4  19597  ptcmplem5  19603  tgpmulg  19639  subgtgp  19651  tgpt0  19664  tsmsxplem2  19703  metss  20058  metustfbasOLD  20115  metustfbas  20116  dscopn  20141  xrsmopn  20364  cncfss  20450  icoopnst  20486  iccpnfcnv  20491  icccvx  20497  evth  20506  phtpycc  20538  pcohtpylem  20566  lmmbrf  20748  fgcfil  20757  caucfil  20769  cfilres  20782  bcth3  20817  ovolfioo  20926  ovolficc  20927  voliunlem3  21008  volcn  21061  mbflimsup  21119  mbfi1fseqlem5  21172  itg2seq  21195  dvnff  21372  dvnadd  21378  cpnord  21384  c1liplem1  21443  plypf1  21655  plyaddlem1  21656  plymullem1  21657  coeeulem  21667  coeidlem  21680  dgrle  21686  plycjlem  21718  elqaalem3  21762  ulmcaulem  21834  ulmcau  21835  psergf  21852  psercn2  21863  efopn  22078  abscxpbnd  22166  leibpi  22312  isppw2  22428  muinv  22508  bposlem3  22600  pntrmax  22788  pntpbnd1  22810  qabvexp  22850  eqeelen  23101  colinearalglem4  23106  axcgrid  23113  axsegconlem1  23114  axsegconlem3  23116  ax5seglem1  23125  ax5seglem2  23126  ax5seglem9  23134  axcontlem2  23162  usgraidx2vlem2  23261  cusgrares  23331  cusgrafilem2  23339  eupath2lem3  23551  grpoidinvlem3  23644  grpoidinv  23646  grpoideu  23647  subgoablo  23749  nmoub3i  24124  nmlno0lem  24144  nmlnoubi  24147  ipasslem3  24184  ipblnfi  24207  hvaddsub4  24431  his35  24441  shsel3  24669  chj4  24889  spansncol  24922  chscllem2  24992  5oalem2  25009  3oalem2  25017  hoaddcl  25113  adjsym  25188  cnvadj  25247  hhcno  25259  hhcnf  25260  nmopub2tALT  25264  unoplin  25275  counop  25276  nmfnleub2  25281  hmoplin  25297  brafnmul  25306  nmlnop0iALT  25350  nmopun  25369  nmophmi  25386  riesz3i  25417  riesz1  25420  cnlnadjlem2  25423  cnlnadjlem6  25427  adjmul  25447  adjadd  25448  bra11  25463  cnvbraval  25465  kbass5  25475  kbass6  25476  leop2  25479  leopadd  25487  leopmuli  25488  leoptri  25491  leopnmid  25493  nmopleid  25494  pj3si  25562  hstel2  25574  cvcon3  25639  dmdmd  25655  dmdbr5  25663  mdsl0  25665  mdslmd1lem1  25680  mdslmd1lem2  25681  mdslmd3i  25687  superpos  25709  chirredlem2  25746  chirredlem3  25747  mdsymlem3  25760  mdsymlem5  25762  mdsymlem6  25763  sumdmdlem  25773  cdjreui  25787  cdj1i  25788  cdj3i  25796  abfmpel  25921  fcomptf  25931  fcnvgreu  25942  xrge0infss  26004  xrge0iifcnv  26315  esumcst  26466  hasheuni  26486  sigaclcu2  26515  insiga  26532  measres  26588  measdivcst  26591  volfiniune  26598  ddemeas  26604  sgn3da  26876  sconpi1  27080  cvmsss2  27115  fprodn0  27441  dfon2lem6  27552  predpo  27596  preddowncl  27608  dftrpred3g  27648  poseq  27665  soseq  27666  nodenselem3  27775  nobndlem6  27789  hfext  28172  fin2solem  28368  fin2so  28369  heicant  28379  mblfinlem2  28382  mblfinlem3  28383  mblfinlem4  28384  ex-ovoliunnfl  28387  mbfresfi  28391  cnambfre  28393  itg2addnclem  28396  itg2addnclem2  28397  itg2addnc  28399  bddiblnc  28415  ftc1anclem3  28422  ftc1anclem4  28423  ftc1anclem5  28424  ftc1anclem6  28425  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  elicc3  28465  fnessref  28518  eqfnun  28568  indexdom  28581  filbcmb  28587  fzadd2  28590  fdc  28594  incsequz  28597  metf1o  28604  caures  28609  bndss  28638  ismtycnv  28654  heiborlem1  28663  rrncmslem  28684  isdrngo2  28717  rngoisocnv  28740  unichnidl  28784  nacsfix  29001  eq0rabdioph  29068  diophren  29105  rencldnfilem  29112  pell1234qrdich  29155  jm2.24  29259  bezoutr1  29282  jm2.26lem3  29303  wepwsolem  29347  pwssplit4  29395  isnumbasgrplem3  29414  dgrnznn  29445  ofsubid  29551  stirlinglem5  29826  2f1fvneq  30096  lswn0  30211  usgra2pthlem1  30253  wlkiswwlk1  30277  el2wlkonot  30341  el2spthonot0  30343  vdcusgra  30484  usgravd00  30491  rusgraprop4  30509  wwlkextproplem3  30515  frgrancvvdeqlemB  30584  frgrawopreglem5  30594  frghash2spot  30609  numclwwlkovf2ex  30632  mat1dimelbas  30790  snlindsntorlem  30893  lshpset2N  32604  pmapglb2N  33255  pmapglb2xN  33256  pclfinN  33384  polval2N  33390  cdleme31fv2  33877  cdleme32fvcl  33924  cdleme48gfv  34021  tendoicl  34280  tendoipl  34281  diaglbN  34540  dochkr1  34963  dochkr1OLDN  34964
  Copyright terms: Public domain W3C validator