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

Theorem adantll 706
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 458 . 2  |-  ( ( th  /\  ph )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 468 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  719  ad2ant2l  738  ad2ant2lr  740  3ad2antl3  1145  3adant1l  1203  ax12eq  2243  ax12el  2244  nfeud2OLD  2278  ralcom2  2875  reu6  3137  sbc2iegf  3249  sbcralt  3255  pofun  4644  tz7.7  4732  onfr  4745  poinxp  4889  xpdifid  5254  sossfld  5273  ssimaex  5744  fndmdif  5795  dffo4  5847  foco2  5851  fcompt  5866  fconst2g  5919  isores3  6013  limsssuc  6450  curry1  6653  curry2  6656  extmptsuppeq  6702  suppss  6708  suppssov1  6710  suppss2  6712  suppssfv  6714  onnseq  6791  oe0  6950  oesuclem  6953  oecl  6965  oaordi  6973  oawordri  6977  oaass  6988  omordi  6993  omword2  7001  omlimcl  7005  odi  7006  omass  7007  oeoe  7026  nnaordi  7045  oaabs  7071  omsmolem  7080  eceqoveq  7193  dom2lem  7337  sbthlem9  7417  php3  7485  onomeneq  7488  isinf  7514  frfi  7545  fiint  7576  fodomfib  7579  fofinf1o  7580  marypha1lem  7671  ordiso2  7717  unwdomg  7787  xpwdomg  7788  ac5num  8194  cff1  8415  cfcoflem  8429  infpssrlem4  8463  isf32lem9  8518  isf34lem7  8536  fin1a2lem13  8569  fin1a2s  8571  hsmexlem4  8586  axdc2lem  8605  zorn2lem6  8658  axpowndlem2  8750  inttsk  8929  tskuni  8938  nqereu  9086  prcdnq  9150  addclprlem2  9174  ltexpri  9200  prlem936  9204  reclem2pr  9205  axsup  9438  add4  9573  ltleadd  9810  lt2mul2div  10196  lediv12a  10213  infmrcl  10297  nn2ge  10335  zextle  10703  fnn0ind  10729  xrlttr  11105  ifle  11155  xaddass  11200  xmulasslem3  11237  xlemul1a  11239  xadddilem  11245  xrsupsslem  11257  xrinfmsslem  11258  supxrunb1  11270  supxrunb2  11271  ixxin  11305  difreicc  11404  iccsplit  11405  iccshftr  11406  iccshftl  11408  iccdil  11410  icccntr  11412  fzaddel  11480  fzrev  11503  modadd1  11729  modmul1  11736  mulexp  11887  expadd  11890  expmul  11893  leexp1a  11906  expnbnd  11977  bccl  12082  hashdom  12126  hashfacen  12191  swrdccat3blem  12370  revccat  12390  2shfti  12553  cau3lem  12826  subcn2  13056  caucvgb  13141  iseraltlem1  13143  sumss  13185  incexclem  13282  supcvg  13301  mertenslem2  13328  eftlcl  13374  reeftlcl  13375  rpnnen2lem6  13485  dvdsext  13567  3dvds  13579  gcdcllem3  13680  seq1st  13729  dvdsprime  13759  pc2dvds  13928  prmpwdvds  13948  unbenlem  13952  infpnlem1  13954  1arith  13971  vdwmc2  14023  ramcl  14073  mrcuni  14542  isacs1i  14578  acsfn  14580  funcpropd  14793  natpropd  14869  curfcl  15025  curf2ndf  15040  resmhm  15469  resmhm2b  15471  mhmco  15472  mhmima  15473  pwsdiagmhm  15479  gsumwsubmcl  15496  gsumwspan  15504  grpissubg  15681  subgint  15685  ghmmhmb  15738  resghm  15743  cntzmhm  15836  symgextf1lem  15905  f1omvdconj  15932  pmtr3ncom  15961  dfod2  16045  gexdvds  16063  subgpgp  16076  sylow1lem3  16079  frgpnabllem1  16331  dprdfeq0  16486  dprdfeq0OLD  16493  isdrng2  16766  cntzsubr  16821  islmodd  16878  lsslss  16964  reslmhm2b  17057  psrbaglefi  17375  psrbaglefiOLD  17376  ply1coe  17643  psgnfix1  17870  psgndif  17874  zrhcopsgndif  17875  ocvocv  17938  frlmsslsp  18065  frlmsslspOLD  18066  frlmlbs  18067  mamudi  18149  mamudir  18150  mulmarep1gsum2  18227  mdetunilem7  18266  mdetunilem9  18268  gsummatr01lem3  18305  smadiadetlem3  18316  elcls  18519  leordtval  18659  cnpnei  18710  cnco  18712  cnss1  18722  cmpsub  18845  hauscmplem  18851  ptbasid  18990  tx2cn  19025  upxp  19038  txindis  19049  xkoptsub  19069  xkopt  19070  trfbas2  19258  filcon  19298  trfil2  19302  filssufilg  19326  ufileu  19334  fixufil  19337  ufilen  19345  rnelfmlem  19367  flimclsi  19393  hauspwpwf1  19402  fclsopn  19429  fclsfnflim  19442  fclscmpi  19444  alexsubALTlem3  19463  alexsubALTlem4  19464  ptcmplem5  19470  tgpmulg  19506  subgtgp  19518  tgpt0  19531  tsmsxplem2  19570  metss  19925  metustfbasOLD  19982  metustfbas  19983  dscopn  20008  xrsmopn  20231  cncfss  20317  icoopnst  20353  iccpnfcnv  20358  icccvx  20364  evth  20373  phtpycc  20405  pcohtpylem  20433  lmmbrf  20615  fgcfil  20624  caucfil  20636  cfilres  20649  bcth3  20684  ovolfioo  20793  ovolficc  20794  voliunlem3  20875  volcn  20928  mbflimsup  20986  mbfi1fseqlem5  21039  itg2seq  21062  dvnff  21239  dvnadd  21245  cpnord  21251  c1liplem1  21310  plypf1  21565  plyaddlem1  21566  plymullem1  21567  coeeulem  21577  coeidlem  21590  dgrle  21596  plycjlem  21628  elqaalem3  21672  ulmcaulem  21744  ulmcau  21745  psergf  21762  psercn2  21773  efopn  21988  abscxpbnd  22076  leibpi  22222  isppw2  22338  muinv  22418  bposlem3  22510  pntrmax  22698  pntpbnd1  22720  qabvexp  22760  eqeelen  22973  colinearalglem4  22978  axcgrid  22985  axsegconlem1  22986  axsegconlem3  22988  ax5seglem1  22997  ax5seglem2  22998  ax5seglem9  23006  axcontlem2  23034  usgraidx2vlem2  23133  cusgrares  23203  cusgrafilem2  23211  eupath2lem3  23423  grpoidinvlem3  23516  grpoidinv  23518  grpoideu  23519  subgoablo  23621  nmoub3i  23996  nmlno0lem  24016  nmlnoubi  24019  ipasslem3  24056  ipblnfi  24079  hvaddsub4  24303  his35  24313  shsel3  24541  chj4  24761  spansncol  24794  chscllem2  24864  5oalem2  24881  3oalem2  24889  hoaddcl  24985  adjsym  25060  cnvadj  25119  hhcno  25131  hhcnf  25132  nmopub2tALT  25136  unoplin  25147  counop  25148  nmfnleub2  25153  hmoplin  25169  brafnmul  25178  nmlnop0iALT  25222  nmopun  25241  nmophmi  25258  riesz3i  25289  riesz1  25292  cnlnadjlem2  25295  cnlnadjlem6  25299  adjmul  25319  adjadd  25320  bra11  25335  cnvbraval  25337  kbass5  25347  kbass6  25348  leop2  25351  leopadd  25359  leopmuli  25360  leoptri  25363  leopnmid  25365  nmopleid  25366  pj3si  25434  hstel2  25446  cvcon3  25511  dmdmd  25527  dmdbr5  25535  mdsl0  25537  mdslmd1lem1  25552  mdslmd1lem2  25553  mdslmd3i  25559  superpos  25581  chirredlem2  25618  chirredlem3  25619  mdsymlem3  25632  mdsymlem5  25634  mdsymlem6  25635  sumdmdlem  25645  cdjreui  25659  cdj1i  25660  cdj3i  25668  abfmpel  25794  fcomptf  25804  fcnvgreu  25815  xrge0iifcnv  26217  esumcst  26368  hasheuni  26388  sigaclcu2  26417  insiga  26434  measres  26490  measdivcst  26493  volfiniune  26500  ddemeas  26506  sgn3da  26772  sconpi1  26976  cvmsss2  27011  fprodn0  27337  dfon2lem6  27448  predpo  27492  preddowncl  27504  dftrpred3g  27544  poseq  27561  soseq  27562  nodenselem3  27671  nobndlem6  27685  hfext  28068  fin2solem  28259  fin2so  28260  heicant  28270  mblfinlem2  28273  mblfinlem3  28274  mblfinlem4  28275  ex-ovoliunnfl  28278  mbfresfi  28282  cnambfre  28284  itg2addnclem  28287  itg2addnclem2  28288  itg2addnc  28290  bddiblnc  28306  ftc1anclem3  28313  ftc1anclem4  28314  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  elicc3  28356  fnessref  28409  eqfnun  28459  indexdom  28472  filbcmb  28478  fzadd2  28481  fdc  28485  incsequz  28488  metf1o  28495  caures  28500  bndss  28529  ismtycnv  28545  heiborlem1  28554  rrncmslem  28575  isdrngo2  28608  rngoisocnv  28631  unichnidl  28675  nacsfix  28893  eq0rabdioph  28960  diophren  28997  rencldnfilem  29004  pell1234qrdich  29047  jm2.24  29151  bezoutr1  29174  jm2.26lem3  29195  wepwsolem  29239  pwssplit4  29287  isnumbasgrplem3  29306  dgrnznn  29337  ofsubid  29443  stirlinglem5  29719  2f1fvneq  29989  lswn0  30104  usgra2pthlem1  30146  wlkiswwlk1  30170  el2wlkonot  30234  el2spthonot0  30236  vdcusgra  30377  usgravd00  30384  rusgraprop4  30402  wwlkextproplem3  30408  frgrancvvdeqlemB  30477  frgrawopreglem5  30487  frghash2spot  30502  numclwwlkovf2ex  30525  snlindsntorlem  30713  lshpset2N  32337  pmapglb2N  32988  pmapglb2xN  32989  pclfinN  33117  polval2N  33123  cdleme31fv2  33610  cdleme32fvcl  33657  cdleme48gfv  33754  tendoicl  34013  tendoipl  34014  diaglbN  34273  dochkr1  34696  dochkr1OLDN  34697
  Copyright terms: Public domain W3C validator