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

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

Proof of Theorem simprll
StepHypRef Expression
1 simpl 483 . 2 ((𝜓𝜒) → 𝜓)
21ad2antrl 724 1 ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  fcof1  7034  mpo0  7228  wfrlem17  7960  eroveu  8381  boxriin  8492  undom  8593  fofinf1o  8787  finsschain  8819  suppeqfsuppbi  8835  fsuppunbi  8842  marypha1lem  8885  wemapsolem  9002  wemapso  9003  wemapso2lem  9004  cantnf  9144  iunfictbso  9528  enfin2i  9731  ttukeylem7  9925  fpwwe2lem2  10042  fpwwe2lem9  10048  fpwwe2lem12  10051  fpwwelem  10055  distrlem4pr  10436  mulcmpblnr  10481  prsrlem1  10482  dedekind  10791  divdivdiv  11329  divmuleq  11333  divadddiv  11343  divsubdiv  11344  lediv12a  11521  xmullem  12645  xlemul1a  12669  seqcaopr  13395  leexp2r  13526  hashf1lem1  13801  hashf1lem2  13802  ccatsymb  13924  wrd2ind  14073  cshweqrep  14171  lo1le  14996  summolem2  15061  summo  15062  prodmolem2  15277  prodmo  15278  bezoutlem3  15877  bezoutlem4  15878  qredeu  15990  pcadd  16213  prmreclem2  16241  vdwlem9  16313  vdwlem10  16314  ramub1lem2  16351  ramub1  16352  prmgaplem7  16381  cofucl  17146  initoeu2  17264  setcmon  17335  poslubmo  17744  posglbmo  17745  issubmd  17959  grprcan  18075  isnsg3  18250  ghmpreima  18318  gaorber  18376  psgneu  18563  odcau  18658  lsmsubm  18707  lsmmod  18730  ablfaclem3  19138  ringpropd  19261  lmodvsmmulgdi  19598  lmodprop2d  19625  lss1d  19664  assamulgscmlem2  20057  mplcoe1  20174  mplcoe5  20177  evlslem1  20223  lindff1  20892  islindf4  20910  mdetunilem7  21155  mdetunilem8  21156  mdetunilem9  21157  mdetuni0  21158  mdetmul  21160  cayhamlem3  21423  ppttop  21543  epttop  21545  cnhaus  21890  isreg2  21913  cncmp  21928  1stcfb  21981  2ndcomap  21994  1stccnp  21998  cldllycmp  22031  1stckgenlem  22089  txcls  22140  ptcnp  22158  txdis1cn  22171  txlly  22172  txnlly  22173  pthaus  22174  txhaus  22183  txkgen  22188  xkohaus  22189  xkococnlem  22195  xkococn  22196  opnfbas  22378  hausflimi  22516  hausflim  22517  hauspwpwf1  22523  alexsubALT  22587  tgpconncomp  22648  qustgplem  22656  metequiv2  23047  met2ndci  23059  nrmmetd  23111  nlmvscnlem1  23222  reconn  23363  xrge0tsms  23369  mulc1cncf  23440  ipcnlem1  23775  minveclem3  23959  pmltpc  23978  ovolicc2lem5  24049  ovolicc2  24050  uniioombllem6  24116  dyadmbllem  24127  vitalilem3  24138  mbfmullem  24253  itg2split  24277  itg2mono  24281  dvlip2  24519  lhop1  24538  dvcnvrelem1  24541  dvfsumrlim  24555  ftc1lem6  24565  itgsubst  24573  dgrco  24792  plyexmo  24829  ulmdvlem3  24917  abelthlem2  24947  abelthlem8  24954  dvdsmulf1o  25698  chpchtsum  25722  dchrptlem2  25768  2sqlem5  25925  2sqlem9  25930  2sqb  25935  chpo1ubb  25984  vmadivsumb  25986  selbergb  26052  selberg2b  26055  selberg3lem2  26061  pntrsumbnd  26069  pntrlog2bnd  26087  pntibndlem3  26095  pnt3  26115  tgjustf  26186  hlcgreu  26331  mirreu3  26367  cgraswap  26533  cgracom  26535  cgratr  26536  flatcgra  26537  acopyeu  26547  axsegcon  26640  ax5seglem9  26650  axeuclid  26676  axcontlem10  26686  axcontlem12  26688  wwlksnredwwlkn0  27601  n4cyclfrgr  27997  frgrnbnb  27999  numclwwlk1lem2fo  28064  ablo4  28254  smcnlem  28401  pjhthmo  29006  pjpjpre  29123  lnconi  29737  resf1o  30392  xrge0tsmsd  30619  derangenlem  32315  pconnconn  32375  connpconn  32379  cvmfolem  32423  cvmliftmolem2  32426  cvmliftmo  32428  cvmliftlem7  32435  cvmlift2lem10  32456  cvmlift3lem8  32470  fpr3g  33019  noresle  33097  linecgr  33439  btwnconn1lem8  33452  btwnconn1lem14  33458  btwnconn3  33461  brsegle  33466  segletr  33472  segleantisym  33473  outsideofeq  33488  linethru  33511  finminlem  33563  nn0prpwlem  33567  neibastop2lem  33605  mblfinlem3  34812  bddiblnc  34843  ftc1cnnc  34847  isbnd3  34943  cvlcvr1  36355  athgt  36472  4atlem12  36628  paddasslem12  36847  paddasslem13  36848  cdleme0cp  37230  cdleme42keg  37502  cdleme42mgN  37504  trlord  37585  cdlemg6c  37636  cdlemkid4  37950  dihopelvalcpre  38264  dihmeetlem1N  38306  dihglblem5apreN  38307  dihmeetlem4preN  38322  dihmeetlem6  38325  dihmeetlem10N  38332  dihmeetlem11N  38333  dihmeetlem13N  38335  dihjatcclem4  38437  mzpcl1  39204  mzpcompact2lem  39226  diophin  39247  pell14qrmulcl  39338  pwssplit4  39567  hbtlem2  39602  iunrelexpuztr  39942  stoweidlem57  42219  stoweidlem61  42223  fourierdlem92  42360  euoreqb  43185  prproropf1olem3  43544  prproropf1olem4  43545  fpprwpprb  43782  rabsubmgmd  43935  2zlidl  44133  lmodvsmdi  44358
  Copyright terms: Public domain W3C validator