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

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

Proof of Theorem simprll
StepHypRef Expression
1 simpl 470 . 2 ((𝜓𝜒) → 𝜓)
21ad2antrl 710 1 ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  fcof1  6769  mpt20  6958  wfrlem17  7670  eroveu  8081  boxriin  8190  undom  8290  fofinf1o  8483  finsschain  8515  suppeqfsuppbi  8531  fsuppunbi  8538  marypha1lem  8581  wemapsolem  8697  wemapso  8698  wemapso2lem  8699  cantnf  8840  iunfictbso  9223  enfin2i  9431  ttukeylem7  9625  fpwwe2lem2  9742  fpwwe2lem9  9748  fpwwe2lem12  9751  fpwwelem  9755  distrlem4pr  10136  mulcmpblnr  10180  prsrlem1  10181  dedekind  10488  divdivdiv  11014  divmuleq  11018  divadddiv  11028  divsubdiv  11029  lediv12a  11204  xmullem  12315  xlemul1a  12339  seqcaopr  13064  leexp2r  13144  hashf1lem1  13459  hashf1lem2  13460  wrd2ind  13704  cshweqrep  13794  lo1le  14608  summolem2  14673  summo  14674  prodmolem2  14889  prodmo  14890  bezoutlem3  15480  bezoutlem4  15481  qredeu  15593  pcadd  15813  prmreclem2  15841  vdwlem9  15913  vdwlem10  15914  ramub1lem2  15951  ramub1  15952  prmgaplem7  15981  cofucl  16755  setcmon  16944  poslubmo  17354  posglbmo  17355  issubmd  17557  grprcan  17663  isnsg3  17833  ghmpreima  17887  gaorber  17945  psgneu  18130  odcau  18223  lsmsubm  18272  lsmmod  18292  ablfaclem3  18691  ringpropd  18787  lmodvsmmulgdi  19105  lmodprop2d  19132  lss1d  19173  assamulgscmlem2  19561  mplcoe1  19677  mplcoe5  19680  evlslem1  19726  lindff1  20373  islindf4  20391  mdetunilem7  20639  mdetunilem8  20640  mdetunilem9  20641  mdetuni0  20642  mdetmul  20644  cayhamlem3  20909  ppttop  21029  epttop  21031  cnhaus  21376  isreg2  21399  cncmp  21413  1stcfb  21466  2ndcomap  21479  1stccnp  21483  cldllycmp  21516  1stckgenlem  21574  txcls  21625  ptcnp  21643  txdis1cn  21656  txlly  21657  txnlly  21658  pthaus  21659  txhaus  21668  txkgen  21673  xkohaus  21674  xkococnlem  21680  xkococn  21681  opnfbas  21863  hausflimi  22001  hausflim  22002  hauspwpwf1  22008  alexsubALT  22072  tgpconncomp  22133  qustgplem  22141  metequiv2  22532  met2ndci  22544  nrmmetd  22596  nlmvscnlem1  22707  reconn  22848  xrge0tsms  22854  mulc1cncf  22925  ipcnlem1  23260  minveclem3  23418  pmltpc  23437  ovolicc2lem5  23508  ovolicc2  23509  uniioombllem6  23575  dyadmbllem  23586  vitalilem3  23597  mbfmullem  23712  itg2split  23736  itg2mono  23740  dvlip2  23978  lhop1  23997  dvcnvrelem1  24000  dvfsumrlim  24014  ftc1lem6  24024  itgsubst  24032  dgrco  24251  plyexmo  24288  ulmdvlem3  24376  abelthlem2  24406  abelthlem8  24413  dvdsmulf1o  25140  chpchtsum  25164  dchrptlem2  25210  2sqlem5  25367  2sqlem9  25372  2sqb  25377  chpo1ubb  25390  vmadivsumb  25392  selbergb  25458  selberg2b  25461  selberg3lem2  25467  pntrsumbnd  25475  pntrlog2bnd  25493  pntibndlem3  25501  pnt3  25521  hlcgreu  25733  mirreu3  25769  cgraswap  25932  cgracom  25934  cgratr  25935  acopyeu  25945  axsegcon  26027  ax5seglem9  26037  axeuclid  26063  axcontlem10  26073  axcontlem12  26075  wwlksnredwwlkn0  27039  frgrnbnb  27474  numclwwlk1lem2fo  27543  ablo4  27739  smcnlem  27886  pjhthmo  28495  pjpjpre  28612  lnconi  29226  resf1o  29838  xrge0tsmsd  30116  derangenlem  31481  pconnconn  31541  connpconn  31545  cvmfolem  31589  cvmliftmolem2  31592  cvmliftmo  31594  cvmliftlem7  31601  cvmlift2lem10  31622  cvmlift3lem8  31636  noresle  32172  linecgr  32514  btwnconn1lem8  32527  btwnconn1lem14  32533  btwnconn3  32536  brsegle  32541  segletr  32547  segleantisym  32548  outsideofeq  32563  linethru  32586  finminlem  32638  nn0prpwlem  32643  neibastop2lem  32681  mblfinlem3  33763  bddiblnc  33794  ftc1cnnc  33798  isbnd3  33896  cvlcvr1  35121  athgt  35238  4atlem12  35394  paddasslem12  35613  paddasslem13  35614  cdleme0cp  35996  cdleme42keg  36268  cdleme42mgN  36270  trlord  36351  cdlemg6c  36402  cdlemkid4  36716  dihopelvalcpre  37030  dihmeetlem1N  37072  dihglblem5apreN  37073  dihmeetlem4preN  37088  dihmeetlem6  37091  dihmeetlem10N  37098  dihmeetlem11N  37099  dihmeetlem13N  37101  dihjatcclem4  37203  mzpcl1  37795  mzpcompact2lem  37817  diophin  37839  pell14qrmulcl  37930  pwssplit4  38161  hbtlem2  38196  iunrelexpuztr  38512  stoweidlem57  40754  stoweidlem61  40758  fourierdlem92  40895  rabsubmgmd  42360  2zlidl  42503  lmodvsmdi  42732
  Copyright terms: Public domain W3C validator