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

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

Proof of Theorem simprll
StepHypRef Expression
1 simpl 472 . 2 ((𝜓𝜒) → 𝜓)
21ad2antrl 764 1 ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  disjxiunOLD  4682  fcof1  6582  mpt20  6767  wfrlem17  7476  eroveu  7885  boxriin  7992  undom  8089  fofinf1o  8282  finsschain  8314  suppeqfsuppbi  8330  fsuppunbi  8337  marypha1lem  8380  wemapsolem  8496  wemapso  8497  wemapso2lem  8498  cantnf  8628  iunfictbso  8975  enfin2i  9181  ttukeylem7  9375  fpwwe2lem2  9492  fpwwe2lem9  9498  fpwwe2lem12  9501  fpwwelem  9505  distrlem4pr  9886  mulcmpblnr  9930  prsrlem1  9931  dedekind  10238  divdivdiv  10764  divmuleq  10768  divadddiv  10778  divsubdiv  10779  lediv12a  10954  xmullem  12132  xlemul1a  12156  seqcaopr  12878  leexp2r  12958  hashf1lem1  13277  hashf1lem2  13278  wrd2ind  13523  cshweqrep  13613  lo1le  14426  summolem2  14491  summo  14492  prodmolem2  14709  prodmo  14710  bezoutlem3  15305  bezoutlem4  15306  qredeu  15419  pcadd  15640  prmreclem2  15668  vdwlem9  15740  vdwlem10  15741  ramub1lem2  15778  ramub1  15779  prmgaplem7  15808  cofucl  16595  setcmon  16784  poslubmo  17193  posglbmo  17194  issubmd  17396  grprcan  17502  isnsg3  17675  ghmpreima  17729  gaorber  17787  psgneu  17972  odcau  18065  lsmsubm  18114  lsmmod  18134  ablfaclem3  18532  ringpropd  18628  lmodvsmmulgdi  18946  lmodprop2d  18973  lss1d  19011  assamulgscmlem2  19397  mplcoe1  19513  mplcoe5  19516  evlslem1  19563  lindff1  20207  islindf4  20225  mdetunilem7  20472  mdetunilem8  20473  mdetunilem9  20474  mdetuni0  20475  mdetmul  20477  cayhamlem3  20740  ppttop  20859  epttop  20861  cnhaus  21206  isreg2  21229  cncmp  21243  1stcfb  21296  2ndcomap  21309  1stccnp  21313  cldllycmp  21346  1stckgenlem  21404  txcls  21455  ptcnp  21473  txdis1cn  21486  txlly  21487  txnlly  21488  pthaus  21489  txhaus  21498  txkgen  21503  xkohaus  21504  xkococnlem  21510  xkococn  21511  opnfbas  21693  hausflimi  21831  hausflim  21832  hauspwpwf1  21838  alexsubALT  21902  tgpconncomp  21963  qustgplem  21971  metequiv2  22362  met2ndci  22374  nrmmetd  22426  nlmvscnlem1  22537  reconn  22678  xrge0tsms  22684  mulc1cncf  22755  ipcnlem1  23090  minveclem3  23246  pmltpc  23265  ovolicc2lem5  23335  ovolicc2  23336  uniioombllem6  23402  dyadmbllem  23413  vitalilem3  23424  mbfmullem  23537  itg2split  23561  itg2mono  23565  dvlip2  23803  lhop1  23822  dvcnvrelem1  23825  dvfsumrlim  23839  ftc1lem6  23849  itgsubst  23857  dgrco  24076  plyexmo  24113  ulmdvlem3  24201  abelthlem2  24231  abelthlem8  24238  dvdsmulf1o  24965  chpchtsum  24989  dchrptlem2  25035  2sqlem5  25192  2sqlem9  25197  2sqb  25202  chpo1ubb  25215  vmadivsumb  25217  selbergb  25283  selberg2b  25286  selberg3lem2  25292  pntrsumbnd  25300  pntrlog2bnd  25318  pntibndlem3  25326  pnt3  25346  hlcgreu  25558  mirreu3  25594  cgraswap  25757  cgracom  25759  cgratr  25760  acopyeu  25770  axsegcon  25852  ax5seglem9  25862  axeuclid  25888  axcontlem10  25898  axcontlem12  25900  wwlksnredwwlkn0  26859  frgrnbnb  27273  numclwlk1lem2fo  27348  ablo4  27532  smcnlem  27680  pjhthmo  28289  pjpjpre  28406  lnconi  29020  resf1o  29633  xrge0tsmsd  29913  derangenlem  31279  pconnconn  31339  connpconn  31343  cvmfolem  31387  cvmliftmolem2  31390  cvmliftmo  31392  cvmliftlem7  31399  cvmlift2lem10  31420  cvmlift3lem8  31434  noresle  31971  linecgr  32313  btwnconn1lem8  32326  btwnconn1lem14  32332  btwnconn3  32335  brsegle  32340  segletr  32346  segleantisym  32347  outsideofeq  32362  linethru  32385  finminlem  32437  nn0prpwlem  32442  neibastop2lem  32480  mblfinlem3  33578  bddiblnc  33610  ftc1cnnc  33614  isbnd3  33713  cvlcvr1  34944  athgt  35060  4atlem12  35216  paddasslem12  35435  paddasslem13  35436  cdleme0cp  35819  cdleme42keg  36091  cdleme42mgN  36093  trlord  36174  cdlemg6c  36225  cdlemkid4  36539  dihopelvalcpre  36854  dihmeetlem1N  36896  dihglblem5apreN  36897  dihmeetlem4preN  36912  dihmeetlem6  36915  dihmeetlem10N  36922  dihmeetlem11N  36923  dihmeetlem13N  36925  dihjatcclem4  37027  mzpcl1  37609  mzpcompact2lem  37631  diophin  37653  pell14qrmulcl  37744  pwssplit4  37976  hbtlem2  38011  iunrelexpuztr  38328  stoweidlem57  40592  stoweidlem61  40596  fourierdlem92  40733  rabsubmgmd  42116  2zlidl  42259  lmodvsmdi  42488
  Copyright terms: Public domain W3C validator