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

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

Proof of Theorem simprll
StepHypRef Expression
1 simpl 471 . 2 ((𝜓𝜒) → 𝜓)
21ad2antrl 759 1 ((𝜑 ∧ ((𝜓𝜒) ∧ 𝜃)) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  disjxiunOLD  4574  fcof1  6420  mpt20  6601  wfrlem17  7295  eroveu  7706  boxriin  7813  undom  7910  fofinf1o  8103  finsschain  8133  suppeqfsuppbi  8149  fsuppunbi  8156  marypha1lem  8199  wemapsolem  8315  wemapso  8316  wemapso2lem  8317  cantnf  8450  iunfictbso  8797  enfin2i  9003  ttukeylem7  9197  fpwwe2lem2  9310  fpwwe2lem9  9316  fpwwe2lem12  9319  fpwwelem  9323  distrlem4pr  9704  mulcmpblnr  9748  prsrlem1  9749  dedekind  10051  divdivdiv  10575  divmuleq  10579  divadddiv  10589  divsubdiv  10590  lediv12a  10765  xmullem  11923  xlemul1a  11947  seqcaopr  12655  leexp2r  12735  hashf1lem1  13048  hashf1lem2  13049  wrd2ind  13275  cshweqrep  13364  lo1le  14176  summolem2  14240  summo  14241  prodmolem2  14450  prodmo  14451  bezoutlem3  15042  bezoutlem4  15043  qredeu  15156  pcadd  15377  prmreclem2  15405  vdwlem9  15477  vdwlem10  15478  ramub1lem2  15515  ramub1  15516  prmgaplem7  15545  cofucl  16317  setcmon  16506  poslubmo  16915  posglbmo  16916  issubmd  17118  grprcan  17224  isnsg3  17397  ghmpreima  17451  gaorber  17510  psgneu  17695  odcau  17788  lsmsubm  17837  lsmmod  17857  ablfaclem3  18255  ringpropd  18351  lmodvsmmulgdi  18667  lmodprop2d  18694  lss1d  18730  assamulgscmlem2  19116  mplcoe1  19232  mplcoe5  19235  evlslem1  19282  lindff1  19920  islindf4  19938  mdetunilem7  20185  mdetunilem8  20186  mdetunilem9  20187  mdetuni0  20188  mdetmul  20190  cayhamlem3  20453  ppttop  20563  epttop  20565  cnhaus  20910  isreg2  20933  cncmp  20947  1stcfb  21000  2ndcomap  21013  1stccnp  21017  cldllycmp  21050  1stckgenlem  21108  txcls  21159  ptcnp  21177  txdis1cn  21190  txlly  21191  txnlly  21192  pthaus  21193  txhaus  21202  txkgen  21207  xkohaus  21208  xkococnlem  21214  xkococn  21215  opnfbas  21398  hausflimi  21536  hausflim  21537  hauspwpwf1  21543  alexsubALT  21607  tgpconcomp  21668  qustgplem  21676  metequiv2  22066  met2ndci  22078  nrmmetd  22130  nlmvscnlem1  22233  reconn  22371  xrge0tsms  22377  mulc1cncf  22447  ipcnlem1  22770  minveclem3  22925  pmltpc  22943  ovolicc2lem5  23013  ovolicc2  23014  uniioombllem6  23079  dyadmbllem  23090  vitalilem3  23102  mbfmullem  23215  itg2split  23239  itg2mono  23243  dvlip2  23479  lhop1  23498  dvcnvrelem1  23501  dvfsumrlim  23515  ftc1lem6  23525  itgsubst  23533  dgrco  23752  plyexmo  23789  ulmdvlem3  23877  abelthlem2  23907  abelthlem8  23914  dvdsmulf1o  24637  chpchtsum  24661  dchrptlem2  24707  2sqlem5  24864  2sqlem9  24869  2sqb  24874  chpo1ubb  24887  vmadivsumb  24889  selbergb  24955  selberg2b  24958  selberg3lem2  24964  pntrsumbnd  24972  pntrlog2bnd  24990  pntibndlem3  24998  pnt3  25018  hlcgreu  25231  mirreu3  25267  cgraswap  25430  cgracom  25432  cgratr  25433  acopyeu  25443  axsegcon  25525  ax5seglem9  25535  axeuclid  25561  axcontlem10  25571  axcontlem12  25573  wwlknredwwlkn0  26021  clwwlkextfrlem1  26369  numclwlk1lem2f1  26387  numclwlk1lem2fo  26388  ablo4  26557  smcnlem  26737  pjhthmo  27351  pjpjpre  27468  lnconi  28082  resf1o  28699  xrge0tsmsd  28922  derangenlem  30213  pconcon  30273  conpcon  30277  cvmfolem  30321  cvmliftmolem2  30324  cvmliftmo  30326  cvmliftlem7  30333  cvmlift2lem10  30354  cvmlift3lem8  30368  linecgr  31164  btwnconn1lem8  31177  btwnconn1lem14  31183  btwnconn3  31186  brsegle  31191  segletr  31197  segleantisym  31198  outsideofeq  31213  linethru  31236  finminlem  31288  nn0prpwlem  31293  neibastop2lem  31331  mblfinlem3  32414  bddiblnc  32446  ftc1cnnc  32450  isbnd3  32549  cvlcvr1  33440  athgt  33556  4atlem12  33712  paddasslem12  33931  paddasslem13  33932  cdleme0cp  34315  cdleme42keg  34588  cdleme42mgN  34590  trlord  34671  cdlemg6c  34722  cdlemkid4  35036  dihopelvalcpre  35351  dihmeetlem1N  35393  dihglblem5apreN  35394  dihmeetlem4preN  35409  dihmeetlem6  35412  dihmeetlem10N  35419  dihmeetlem11N  35420  dihmeetlem13N  35422  dihjatcclem4  35524  mzpcl1  36106  mzpcompact2lem  36128  diophin  36150  pell14qrmulcl  36241  pwssplit4  36473  hbtlem2  36509  iunrelexpuztr  36826  stoweidlem57  38747  stoweidlem61  38751  fourierdlem92  38888  wwlksnredwwlkn0  41097  frgrnbnb  41458  av-numclwlk1lem2f1  41519  av-numclwlk1lem2fo  41520  rabsubmgmd  41576  2zlidl  41719  lmodvsmdi  41952
  Copyright terms: Public domain W3C validator