MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantll Structured version   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  2269  ax11el  2270  nfeud2  2292  ralcom2  2864  reu6  3115  sbc2iegf  3219  sbcralt  3225  pofun  4511  tz7.7  4599  onfr  4612  limsssuc  4822  poinxp  4933  sossfld  5309  ssimaex  5780  fndmdif  5826  dffo4  5877  foco2  5881  fcompt  5896  fconst2g  5938  isores3  6047  curry1  6430  curry2  6433  onnseq  6598  oe0  6758  oesuclem  6761  oecl  6773  oaordi  6781  oawordri  6785  oaass  6796  omordi  6801  omword2  6809  omlimcl  6813  odi  6814  omass  6815  oeoe  6834  nnaordi  6853  oaabs  6879  omsmolem  6888  eceqoveq  7001  dom2lem  7139  sbthlem9  7217  php3  7285  onomeneq  7288  isinf  7314  frfi  7344  fiint  7375  fodomfib  7378  fofinf1o  7379  marypha1lem  7430  ordiso2  7476  unwdomg  7544  xpwdomg  7545  ac5num  7909  cff1  8130  cfcoflem  8144  infpssrlem4  8178  isf32lem9  8233  isf34lem7  8251  fin1a2lem13  8284  fin1a2s  8286  hsmexlem4  8301  axdc2lem  8320  zorn2lem6  8373  inttsk  8641  tskuni  8650  nqereu  8798  prcdnq  8862  addclprlem2  8886  ltexpri  8912  prlem936  8916  reclem2pr  8917  axsup  9143  add4  9273  ltleadd  9503  lt2mul2div  9878  lediv12a  9895  infmrcl  9979  nn2ge  10017  zextle  10335  fnn0ind  10361  xrlttr  10725  ifle  10775  xaddass  10820  xmulasslem3  10857  xlemul1a  10859  xadddilem  10865  xrsupsslem  10877  xrinfmsslem  10878  supxrunb1  10890  supxrunb2  10891  ixxin  10925  difreicc  11020  iccsplit  11021  iccshftr  11022  iccshftl  11024  iccdil  11026  icccntr  11028  fzaddel  11079  fzrev  11100  modadd1  11270  modmul1  11271  mulexp  11411  expadd  11414  expmul  11417  leexp1a  11430  expnbnd  11500  bccl  11605  hashdom  11645  hashfacen  11695  revccat  11790  2shfti  11887  cau3lem  12150  subcn2  12380  caucvgb  12465  iseraltlem1  12467  sumss  12510  incexclem  12608  supcvg  12627  mertenslem2  12654  eftlcl  12700  reeftlcl  12701  rpnnen2lem6  12811  dvdsext  12892  3dvds  12904  gcdcllem3  13005  seq1st  13054  dvdsprime  13084  pc2dvds  13244  prmpwdvds  13264  unbenlem  13268  infpnlem1  13270  1arith  13287  vdwmc2  13339  ramcl  13389  mrcuni  13838  isacs1i  13874  acsfn  13876  funcpropd  14089  natpropd  14165  curfcl  14321  curf2ndf  14336  spwpr2  14652  resmhm  14751  resmhm2b  14753  mhmco  14754  mhmima  14755  pwsdiagmhm  14760  gsumwsubmcl  14776  gsumwspan  14783  subgint  14956  ghmmhmb  15009  resghm  15014  cntzmhm  15129  dfod2  15192  gexdvds  15210  subgpgp  15223  sylow1lem3  15226  frgpnabllem1  15476  dprdfeq0  15572  isdrng2  15837  cntzsubr  15892  islmodd  15948  lsslss  16029  reslmhm2b  16122  psrbaglefi  16429  ply1coe  16676  ocvocv  16890  elcls  17129  leordtval  17269  cnpnei  17320  cnco  17322  cnss1  17332  cmpsub  17455  hauscmplem  17461  ptbasid  17599  tx2cn  17634  upxp  17647  txindis  17658  xkoptsub  17678  xkopt  17679  trfbas2  17867  filcon  17907  trfil2  17911  filssufilg  17935  ufileu  17943  fixufil  17946  ufilen  17954  rnelfmlem  17976  flimclsi  18002  hauspwpwf1  18011  fclsopn  18038  fclsfnflim  18051  fclscmpi  18053  alexsubALTlem3  18072  alexsubALTlem4  18073  ptcmplem5  18079  tgpmulg  18115  subgtgp  18127  tgpt0  18140  tsmsxplem2  18175  metss  18530  metustfbasOLD  18587  metustfbas  18588  dscopn  18613  xrsmopn  18835  cncfss  18921  icoopnst  18956  iccpnfcnv  18961  icccvx  18967  evth  18976  phtpycc  19008  pcohtpylem  19036  lmmbrf  19207  fgcfil  19216  caucfil  19228  cfilres  19241  bcth3  19276  ovolfioo  19356  ovolficc  19357  voliunlem3  19438  volcn  19490  mbflimsup  19550  mbfi1fseqlem5  19603  itg2seq  19626  dvnff  19801  dvnadd  19807  cpnord  19813  c1liplem1  19872  plypf1  20123  plyaddlem1  20124  plymullem1  20125  coeeulem  20135  coeidlem  20148  dgrle  20154  plycjlem  20186  elqaalem3  20230  ulmcaulem  20302  ulmcau  20303  psergf  20320  psercn2  20331  efopn  20541  abscxpbnd  20629  leibpi  20774  isppw2  20890  muinv  20970  bposlem3  21062  pntrmax  21250  pntpbnd1  21272  qabvexp  21312  usgraidx2vlem2  21403  cusgrares  21473  cusgrafilem2  21481  eupath2lem3  21693  grpoidinvlem3  21786  grpoidinv  21788  grpoideu  21789  subgoablo  21891  nmoub3i  22266  nmlno0lem  22286  nmlnoubi  22289  ipasslem3  22326  ipblnfi  22349  hvaddsub4  22572  his35  22582  shsel3  22809  chj4  23029  spansncol  23062  chscllem2  23132  5oalem2  23149  3oalem2  23157  hoaddcl  23253  adjsym  23328  cnvadj  23387  hhcno  23399  hhcnf  23400  nmopub2tALT  23404  unoplin  23415  counop  23416  nmfnleub2  23421  hmoplin  23437  brafnmul  23446  nmlnop0iALT  23490  nmopun  23509  nmophmi  23526  riesz3i  23557  riesz1  23560  cnlnadjlem2  23563  cnlnadjlem6  23567  adjmul  23587  adjadd  23588  bra11  23603  cnvbraval  23605  kbass5  23615  kbass6  23616  leop2  23619  leopadd  23627  leopmuli  23628  leoptri  23631  leopnmid  23633  nmopleid  23634  pj3si  23702  hstel2  23714  cvcon3  23779  dmdmd  23795  dmdbr5  23803  mdsl0  23805  mdslmd1lem1  23820  mdslmd1lem2  23821  mdslmd3i  23827  superpos  23849  chirredlem2  23886  chirredlem3  23887  mdsymlem3  23900  mdsymlem5  23902  mdsymlem6  23903  sumdmdlem  23913  cdjreui  23927  cdj1i  23928  cdj3i  23936  abfmpel  24059  fcomptf  24069  xrge0iifcnv  24311  esumcst  24447  hasheuni  24467  sigaclcu2  24495  insiga  24512  measres  24568  measdivcst  24571  volfiniune  24578  sconpi1  24918  cvmsss2  24953  fprodn0  25295  dfon2lem6  25407  predpo  25451  preddowncl  25463  dftrpred3g  25503  poseq  25520  soseq  25521  nodenselem3  25630  nobndlem6  25644  eqeelen  25835  colinearalglem4  25840  axcgrid  25847  axsegconlem1  25848  axsegconlem3  25850  ax5seglem1  25859  ax5seglem2  25860  ax5seglem9  25868  axcontlem2  25896  hfext  26116  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  ex-ovoliunnfl  26239  mbfresfi  26243  cnambfre  26245  itg2addnclem  26246  itg2addnclem2  26247  itg2addnc  26249  bddiblnc  26265  ftc1anclem3  26272  ftc1anclem4  26273  ftc1anclem5  26274  ftc1anclem6  26275  ftc1anclem7  26276  ftc1anclem8  26277  ftc1anc  26278  elicc3  26311  fnessref  26364  eqfnun  26414  indexdom  26427  filbcmb  26433  fzadd2  26436  fdc  26440  incsequz  26443  metf1o  26452  caures  26457  bndss  26486  ismtycnv  26502  heiborlem1  26511  rrncmslem  26532  isdrngo2  26565  rngoisocnv  26588  unichnidl  26632  nacsfix  26757  eq0rabdioph  26826  diophren  26865  rencldnfilem  26872  pell1234qrdich  26915  jm2.24  27019  bezoutr1  27042  jm2.26lem3  27063  wepwsolem  27107  pwssplit4  27159  frlmsslsp  27216  frlmlbs  27217  isnumbasgrplem3  27238  dgrnznn  27308  f1omvdconj  27357  mamudi  27429  mamudir  27430  ofsubid  27509  stirlinglem5  27794  2f1fvneq  28063  swrdccat3blem  28184  2cshw1lem1  28214  lswrdn0  28226  usgra2pthlem1  28263  el2wlkonot  28289  el2spthonot0  28291  frgrancvvdeqlemB  28364  frgrawopreglem5  28374  frghash2spot  28389  lshpset2N  29854  pmapglb2N  30505  pmapglb2xN  30506  pclfinN  30634  polval2N  30640  cdleme31fv2  31127  cdleme32fvcl  31174  cdleme48gfv  31271  tendoicl  31530  tendoipl  31531  diaglbN  31790  dochkr1  32213  dochkr1OLDN  32214
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