MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simprll Structured version   Visualization version   GIF version

Theorem simprll 778
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprll ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜓)

Proof of Theorem simprll
StepHypRef Expression
1 simpl 484 . 2 ((𝜓𝜒) → 𝜓)
21ad2antrl 727 1 ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  fcof1  7234  mpo0  7443  fpr3g  8217  fprresex  8242  wfrlem17OLD  8272  eroveu  8754  boxriin  8881  undomOLD  9007  fofinf1o  9274  finsschain  9306  suppeqfsuppbi  9324  fsuppunbi  9331  marypha1lem  9374  wemapsolem  9491  wemapso  9492  wemapso2lem  9493  cantnf  9634  iunfictbso  10055  enfin2i  10262  ttukeylem7  10456  fpwwe2lem2  10573  fpwwe2lem8  10579  fpwwe2lem11  10582  fpwwelem  10586  distrlem4pr  10967  mulcmpblnr  11012  prsrlem1  11013  dedekind  11323  divdivdiv  11861  divmuleq  11865  divadddiv  11875  divsubdiv  11876  lediv12a  12053  xmullem  13189  xlemul1a  13213  seqcaopr  13951  leexp2r  14085  hashf1lem1  14359  hashf1lem1OLD  14360  hashf1lem2  14361  ccatsymb  14476  wrd2ind  14617  cshweqrep  14715  rtrclreclem4  14952  lo1le  15542  summolem2  15606  summo  15607  prodmolem2  15823  prodmo  15824  bezoutlem3  16427  bezoutlem4  16428  qredeu  16539  pcadd  16766  prmreclem2  16794  vdwlem9  16866  vdwlem10  16867  ramub1lem2  16904  ramub1  16905  prmgaplem7  16934  cofucl  17779  initoeu2  17907  setcmon  17978  poslubmo  18305  posglbmo  18306  issubmd  18622  grprcan  18789  isnsg3  18967  ghmpreima  19035  gaorber  19093  psgneu  19293  odcau  19391  lsmsubm  19440  lsmmod  19462  ablfaclem3  19871  ringpropd  20011  lmodvsmmulgdi  20372  lmodprop2d  20399  lss1d  20439  lindff1  21242  islindf4  21260  assamulgscmlem2  21319  mplcoe1  21454  mplcoe5  21457  evlslem1  21508  mdetunilem7  21983  mdetunilem8  21984  mdetunilem9  21985  mdetuni0  21986  mdetmul  21988  cayhamlem3  22252  ppttop  22373  epttop  22375  cnhaus  22721  isreg2  22744  cncmp  22759  1stcfb  22812  2ndcomap  22825  1stccnp  22829  cldllycmp  22862  1stckgenlem  22920  txcls  22971  ptcnp  22989  txdis1cn  23002  txlly  23003  txnlly  23004  pthaus  23005  txhaus  23014  txkgen  23019  xkohaus  23020  xkococnlem  23026  xkococn  23027  opnfbas  23209  hausflimi  23347  hausflim  23348  hauspwpwf1  23354  alexsubALT  23418  tgpconncomp  23480  qustgplem  23488  metequiv2  23882  met2ndci  23894  nrmmetd  23946  nlmvscnlem1  24066  reconn  24207  xrge0tsms  24213  mulc1cncf  24284  ipcnlem1  24625  minveclem3  24809  pmltpc  24830  ovolicc2lem5  24901  ovolicc2  24902  uniioombllem6  24968  dyadmbllem  24979  vitalilem3  24990  mbfmullem  25106  itg2split  25130  itg2mono  25134  bddiblnc  25222  dvlip2  25375  lhop1  25394  dvcnvrelem1  25397  dvfsumrlim  25411  ftc1lem6  25421  itgsubst  25429  dgrco  25652  plyexmo  25689  ulmdvlem3  25777  abelthlem2  25807  abelthlem8  25814  dvdsmulf1o  26559  chpchtsum  26583  dchrptlem2  26629  2sqlem5  26786  2sqlem9  26791  2sqb  26796  chpo1ubb  26845  vmadivsumb  26847  selbergb  26913  selberg2b  26916  selberg3lem2  26922  pntrsumbnd  26930  pntrlog2bnd  26948  pntibndlem3  26956  pnt3  26976  noresle  27061  nosupprefixmo  27064  noinfprefixmo  27065  nosupbday  27069  noinfbday  27084  noinfbnd1lem5  27091  addsprop  27310  tgjustf  27457  hlcgreu  27602  mirreu3  27638  cgraswap  27804  cgracom  27806  cgratr  27807  flatcgra  27808  acopyeu  27818  axsegcon  27918  ax5seglem9  27928  axeuclid  27954  axcontlem10  27964  axcontlem12  27966  wwlksnredwwlkn0  28883  n4cyclfrgr  29277  frgrnbnb  29279  numclwwlk1lem2fo  29344  ablo4  29534  smcnlem  29681  pjhthmo  30286  pjpjpre  30403  lnconi  31017  resf1o  31694  mgcoval  31895  xrge0tsmsd  31948  derangenlem  33822  pconnconn  33882  connpconn  33886  cvmfolem  33930  cvmliftmolem2  33933  cvmliftmo  33935  cvmliftlem7  33942  cvmlift2lem10  33963  cvmlift3lem8  33977  linecgr  34712  btwnconn1lem8  34725  btwnconn1lem14  34731  btwnconn3  34734  brsegle  34739  segletr  34745  segleantisym  34746  outsideofeq  34761  linethru  34784  finminlem  34836  nn0prpwlem  34840  neibastop2lem  34878  mblfinlem3  36163  ftc1cnnc  36196  isbnd3  36289  cvlcvr1  37847  athgt  37965  4atlem12  38121  paddasslem12  38340  paddasslem13  38341  cdleme0cp  38723  cdleme42keg  38995  cdleme42mgN  38997  trlord  39078  cdlemg6c  39129  cdlemkid4  39443  dihopelvalcpre  39757  dihmeetlem1N  39799  dihglblem5apreN  39800  dihmeetlem4preN  39815  dihmeetlem6  39818  dihmeetlem10N  39825  dihmeetlem11N  39826  dihmeetlem13N  39828  dihjatcclem4  39930  fsuppssind  40811  prjspner1  41007  mzpcl1  41095  mzpcompact2lem  41117  diophin  41138  pell14qrmulcl  41229  pwssplit4  41459  hbtlem2  41494  iunrelexpuztr  42079  stoweidlem57  44384  stoweidlem61  44388  fourierdlem92  44525  euoreqb  45427  prproropf1olem3  45783  prproropf1olem4  45784  fpprwpprb  46018  rabsubmgmd  46171  2zlidl  46318  lmodvsmdi  46544
  Copyright terms: Public domain W3C validator