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

Theorem adantll 711
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 459 . 2  |-  ( ( th  /\  ph )  ->  ph )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan 469 1  |-  ( ( ( th  /\  ph )  /\  ps )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  ad2antlr  724  ad2ant2l  743  ad2ant2lr  745  3ad2antl3  1158  3adant1l  1218  ralcom2  2947  reu6  3213  sbc2iegf  3319  sbcralt  3325  pofun  4730  tz7.7  4818  onfr  4831  poinxp  4977  xpdifid  5345  sossfld  5363  ssimaex  5839  fndmdif  5893  dffo4  5949  foco2  5953  fcompt  5969  fconst2g  6028  isores3  6132  limsssuc  6584  curry1  6791  curry2  6794  extmptsuppeq  6842  suppss  6848  suppssov1  6850  suppss2  6852  suppssfv  6854  onnseq  6933  oe0  7090  oesuclem  7093  oecl  7105  oaordi  7113  oawordri  7117  oaass  7128  omordi  7133  omword2  7141  omlimcl  7145  odi  7146  omass  7147  oeoe  7166  nnaordi  7185  oaabs  7211  omsmolem  7220  eceqoveq  7334  dom2lem  7474  sbthlem9  7554  php3  7622  onomeneq  7626  isinf  7649  frfi  7680  fiint  7712  fodomfib  7715  fofinf1o  7716  marypha1lem  7808  ordiso2  7855  unwdomg  7925  xpwdomg  7926  ac5num  8330  cff1  8551  cfcoflem  8565  infpssrlem4  8599  isf32lem9  8654  isf34lem7  8672  fin1a2lem13  8705  fin1a2s  8707  hsmexlem4  8722  axdc2lem  8741  zorn2lem6  8794  axpowndlem2  8886  inttsk  9063  tskuni  9072  nqereu  9218  prcdnq  9282  addclprlem2  9306  ltexpri  9332  prlem936  9336  reclem2pr  9337  axsup  9571  add4  9707  ltleadd  9953  lt2mul2div  10337  lediv12a  10354  infmrcl  10438  nn2ge  10477  zextle  10853  fnn0ind  10878  xrlttr  11267  ifle  11317  xaddass  11362  xmulasslem3  11399  xlemul1a  11401  xadddilem  11407  xrsupsslem  11419  xrinfmsslem  11420  supxrunb1  11432  supxrunb2  11433  ixxin  11467  difreicc  11573  iccsplit  11574  iccshftr  11575  iccshftl  11577  iccdil  11579  icccntr  11581  fzaddel  11640  fzrev  11664  modadd1  11934  modmul1  11943  mulexp  12108  expadd  12111  expmul  12114  leexp1a  12127  expnbnd  12197  bccl  12302  hashdom  12350  hashfacen  12407  wrdnval  12479  swrdccat3blem  12631  revccat  12651  2shfti  12915  rexico  13188  cau3lem  13189  subcn2  13419  caucvgb  13504  iseraltlem1  13506  sumss  13548  incexclem  13650  supcvg  13669  mertenslem2  13696  fprodn0  13785  eftlcl  13844  reeftlcl  13845  rpnnen2lem6  13955  dvdsext  14039  3dvds  14052  gcdcllem3  14153  seq1st  14202  dvdsprime  14232  pc2dvds  14404  prmpwdvds  14424  unbenlem  14428  infpnlem1  14430  1arith  14447  vdwmc2  14499  ramcl  14549  mrcuni  15028  isacs1i  15064  acsfn  15066  funcpropd  15306  natpropd  15382  curfcl  15618  curf2ndf  15633  resmhm  16107  resmhm2b  16109  mhmco  16110  mhmima  16111  pwsdiagmhm  16117  gsumwsubmcl  16123  gsumwspan  16131  grpissubg  16338  subgint  16342  ghmmhmb  16395  resghm  16400  cntzmhm  16493  symgextf1lem  16562  f1omvdconj  16588  pmtr3ncom  16617  dfod2  16703  gexdvds  16721  subgpgp  16734  sylow1lem3  16737  frgpnabllem1  16994  dprdfeq0  17175  dprdfeq0OLD  17182  isdrng2  17519  cntzsubr  17574  islmodd  17631  lsslss  17720  reslmhm2b  17813  psrbaglefi  18136  psrbaglefiOLD  18137  mptcoe1fsupp  18368  ply1coe  18450  ply1coeOLD  18451  psgnfix1  18725  psgndif  18729  zrhcopsgndif  18730  ocvocv  18793  frlmsslsp  18916  frlmlbs  18917  mamudi  18990  mamudir  18991  mat1dimelbas  19058  scmatmulcl  19105  scmatfo  19117  mulmarep1gsum2  19161  mdetunilem7  19205  mdetunilem9  19207  gsummatr01lem3  19244  smadiadetlem3  19255  mp2pm2mplem4  19395  chfacfisf  19440  chfacfisfcpmat  19441  cpmadugsumlemF  19462  elcls  19660  leordtval  19800  cnpnei  19851  cnco  19853  cnss1  19863  cmpsub  19986  hauscmplem  19992  dissnlocfin  20115  ptbasid  20161  tx2cn  20196  upxp  20209  txindis  20220  xkoptsub  20240  xkopt  20241  trfbas2  20429  filcon  20469  trfil2  20473  filssufilg  20497  ufileu  20505  fixufil  20508  ufilen  20516  rnelfmlem  20538  flimclsi  20564  hauspwpwf1  20573  fclsopn  20600  fclsfnflim  20613  fclscmpi  20615  alexsubALTlem3  20634  alexsubALTlem4  20635  ptcmplem5  20641  tgpmulg  20677  subgtgp  20689  tgpt0  20702  tsmsxplem2  20741  metss  21096  metustfbasOLD  21153  metustfbas  21154  dscopn  21179  xrsmopn  21402  cncfss  21488  icoopnst  21524  iccpnfcnv  21529  icccvx  21535  evth  21544  phtpycc  21576  pcohtpylem  21604  lmmbrf  21786  fgcfil  21795  caucfil  21807  cfilres  21820  bcth3  21855  ovolfioo  21964  ovolficc  21965  voliunlem3  22047  volcn  22100  mbflimsup  22158  mbfi1fseqlem5  22211  itg2seq  22234  dvnff  22411  dvnadd  22417  cpnord  22423  c1liplem1  22482  plypf1  22694  plyaddlem1  22695  plymullem1  22696  coeeulem  22706  coeidlem  22719  dgrle  22725  dgrnznn  22729  plycjlem  22758  elqaalem3  22802  ulmcaulem  22874  ulmcau  22875  psergf  22892  psercn2  22903  efopn  23126  abscxpbnd  23214  leibpi  23389  isppw2  23506  muinv  23586  bposlem3  23678  pntrmax  23866  pntpbnd1  23888  qabvexp  23928  eqeelen  24328  colinearalglem4  24333  axcgrid  24340  axsegconlem1  24341  axsegconlem3  24343  ax5seglem1  24352  ax5seglem2  24353  ax5seglem9  24361  axcontlem2  24389  usgraidx2vlem2  24513  cusgrares  24593  cusgrafilem2  24601  wlkiswwlk1  24811  wwlkextproplem3  24864  el2wlkonot  24990  el2spthonot0  24992  usgravd00  25040  rusgraprop4  25065  eupath2lem3  25100  frgrancvvdeqlemB  25159  frgrawopreglem5  25169  frghash2spot  25184  numclwwlkovf2ex  25207  grpoidinvlem3  25325  grpoidinv  25327  grpoideu  25328  subgoablo  25430  nmoub3i  25805  nmlno0lem  25825  nmlnoubi  25828  ipasslem3  25865  ipblnfi  25888  hvaddsub4  26112  his35  26122  shsel3  26350  chj4  26570  spansncol  26603  chscllem2  26673  5oalem2  26690  3oalem2  26698  hoaddcl  26793  adjsym  26868  cnvadj  26927  hhcno  26939  hhcnf  26940  nmopub2tALT  26944  unoplin  26955  counop  26956  nmfnleub2  26961  hmoplin  26977  brafnmul  26986  nmlnop0iALT  27030  nmopun  27049  nmophmi  27066  riesz3i  27097  riesz1  27100  cnlnadjlem2  27103  cnlnadjlem6  27107  adjmul  27127  adjadd  27128  bra11  27143  cnvbraval  27145  kbass5  27155  kbass6  27156  leop2  27159  leopadd  27167  leopmuli  27168  leoptri  27171  leopnmid  27173  nmopleid  27174  pj3si  27242  hstel2  27254  cvcon3  27319  dmdmd  27335  dmdbr5  27343  mdsl0  27345  mdslmd1lem1  27360  mdslmd1lem2  27361  mdslmd3i  27367  superpos  27389  chirredlem2  27426  chirredlem3  27427  mdsymlem3  27440  mdsymlem5  27442  mdsymlem6  27443  sumdmdlem  27453  cdjreui  27467  cdj1i  27468  cdj3i  27476  foresf1o  27521  abfmpel  27633  fcomptf  27644  fcnvgreu  27660  xrge0infss  27730  cmpcref  28007  xrge0iifcnv  28069  esumcst  28211  hasheuni  28233  esum2dlem  28240  esum2d  28241  sigaclcu2  28269  insiga  28286  measres  28349  measdivcst  28352  volfiniune  28358  ddemeas  28364  sgn3da  28663  sconpi1  28873  cvmsss2  28908  mrsubco  29070  dfon2lem6  29385  predpo  29429  preddowncl  29441  dftrpred3g  29481  poseq  29498  soseq  29499  nodenselem3  29608  nobndlem6  29622  hfext  29993  fin2solem  30204  fin2so  30205  heicant  30214  mblfinlem2  30217  mblfinlem3  30218  mblfinlem4  30219  ex-ovoliunnfl  30222  mbfresfi  30226  cnambfre  30228  itg2addnclem  30232  itg2addnclem2  30233  itg2addnc  30235  bddiblnc  30251  ftc1anclem3  30258  ftc1anclem4  30259  ftc1anclem5  30260  ftc1anclem6  30261  ftc1anclem7  30262  ftc1anclem8  30263  ftc1anc  30264  elicc3  30301  fnessref  30341  eqfnun  30378  indexdom  30391  filbcmb  30397  fzadd2  30400  fdc  30404  incsequz  30407  metf1o  30414  caures  30419  bndss  30448  ismtycnv  30464  heiborlem1  30473  rrncmslem  30494  isdrngo2  30527  rngoisocnv  30550  unichnidl  30594  nacsfix  30810  eq0rabdioph  30875  diophren  30912  rencldnfilem  30919  pell1234qrdich  30962  jm2.24  31066  bezoutr1  31089  jm2.26lem3  31109  wepwsolem  31153  pwssplit4  31201  isnumbasgrplem3  31222  cvgdvgrat  31362  dvdslcm  31372  lcmeq0  31374  lcmcl  31375  lcmneg  31377  lcmdvds  31382  ofsubid  31397  bcc0  31413  binomcxplemnn0  31422  ssfiunibd  31675  fsumsplitsn  31737  fprodsplitsn  31758  fprodle  31770  divcnvg  31799  limcrecl  31801  sumnnodd  31802  islpcn  31811  lptre2pt  31812  limcresiooub  31814  limcresioolb  31815  limclner  31823  cncfuni  31855  icccncfext  31856  cncficcgt0  31857  cncfiooicclem1  31862  cncfiooiccre  31864  dvasinbx  31883  dvdsn1add  31902  dvnmul  31906  dvmptfprodlem  31907  dvnprodlem1  31909  dvnprodlem3  31911  iblspltprt  31938  itgioocnicc  31942  itgspltprt  31944  stirlinglem5  32026  dirker2re  32040  dirkerper  32044  dirkertrigeq  32049  dirkercncflem2  32052  fourierdlem12  32067  fourierdlem15  32070  fourierdlem16  32071  fourierdlem20  32075  fourierdlem21  32076  fourierdlem22  32077  fourierdlem39  32094  fourierdlem40  32095  fourierdlem41  32096  fourierdlem42  32097  fourierdlem46  32101  fourierdlem49  32104  fourierdlem50  32105  fourierdlem57  32112  fourierdlem58  32113  fourierdlem59  32114  fourierdlem64  32119  fourierdlem65  32120  fourierdlem66  32121  fourierdlem68  32123  fourierdlem70  32125  fourierdlem71  32126  fourierdlem73  32128  fourierdlem78  32133  fourierdlem79  32134  fourierdlem80  32135  fourierdlem81  32136  fourierdlem82  32137  fourierdlem83  32138  fourierdlem87  32142  fourierdlem93  32148  fourierdlem95  32150  fourierdlem101  32156  fourierdlem103  32158  fourierdlem104  32159  fourierdlem111  32166  fourierdlem112  32167  sqwvfoura  32177  fourierswlem  32179  elaa2lem  32182  etransclem13  32196  etransclem23  32206  etransclem24  32207  etransclem32  32215  etransclem38  32221  etransclem46  32229  lswn0  32554  2f1fvneq  32628  usgra2pthlem1  32671  vdcusgra  32677  resmgmhm  32804  resmgmhm2b  32806  mgmhmco  32807  mgmhmima  32808  snlindsntorlem  33271  aacllem  33550  ax12eq  35084  ax12el  35085  lshpset2N  35257  pmapglb2N  35908  pmapglb2xN  35909  pclfinN  36037  polval2N  36043  cdleme31fv2  36532  cdleme32fvcl  36579  cdleme48gfv  36676  tendoicl  36935  tendoipl  36936  diaglbN  37195  dochkr1  37618  dochkr1OLDN  37619
  Copyright terms: Public domain W3C validator