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

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

Proof of Theorem simprrr
StepHypRef Expression
1 simpr 475 . 2 ((𝜒𝜃) → 𝜃)
21ad2antll 760 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:  f1prex  6416  fliftfun  6439  grpridd  6749  wfrlem17  7295  mapdom2  7993  domunfican  8095  fofinf1o  8103  finsschain  8133  wemaplem3  8313  oemapvali  8441  iunfictbso  8797  enfin2i  9003  fin1a2s  9096  distrlem4pr  9704  mulcmpblnr  9748  prsrlem1  9749  addsrmo  9750  mulsrmo  9751  divdivdiv  10577  divsubdiv  10592  lediv12a  10767  xralrple  11871  seqcaopr  12657  leexp2r  12737  hashbclem  13047  wrd2ind  13277  cshwidxmod  13348  rtrclreclem4  13597  relexpindlem  13599  rtrclind  13601  rlimresb  14092  summo  14243  fsum2dlem  14291  prodmo  14453  fprod2dlem  14497  bezoutlem3  15044  bezoutlem4  15045  qredeu  15158  coprmproddvdslem  15162  pcqmul  15344  pcadd  15379  pockthg  15396  ramub1lem2  15517  cshwsdisj  15591  mreexexlem4d  16078  issubc3  16280  cofucl  16319  setcmon  16508  setcepi  16509  drsdirfi  16709  poslubmo  16917  posglbmo  16918  ghmpreima  17453  gaorber  17512  psgnunilem4  17688  psgneu  17697  odcau  17790  pgpssslw  17800  fislw  17811  lsmsubm  17839  efgsfo  17923  pgpfac1  18250  pgpfaclem2  18252  pgpfaclem3  18253  unitgrp  18438  islmodd  18640  lmodprop2d  18696  lsspropd  18786  lbsextlem4  18930  assapropd  19096  evlslem1  19284  mdetunilem8  20191  mdetmul  20195  ppttop  20568  epttop  20570  restbas  20719  iscnp4  20824  cnpco  20828  nrmsep  20918  regsep2  20937  ordthauslem  20944  1stcfb  21005  2ndcctbss  21015  2ndcdisj  21016  2ndcomap  21018  dis2ndc  21020  1stcelcls  21021  nlly2i  21036  islly2  21044  hausllycmp  21054  lly1stc  21056  comppfsc  21092  1stckgenlem  21113  ptbasin  21137  txcls  21164  ptcnp  21182  txlly  21196  txnlly  21197  txtube  21200  txcmplem1  21201  txcmplem2  21202  xkococnlem  21219  basqtop  21271  regr1lem  21299  kqreglem1  21301  kqreglem2  21302  kqnrmlem1  21303  kqnrmlem2  21304  reghmph  21353  nrmhmph  21354  filuni  21446  rnelfmlem  21513  fmufil  21520  fclscf  21586  fclsfnflim  21588  flimfnfcls  21589  uffclsflim  21592  cnpfcfi  21601  cnpfcf  21602  alexsublem  21605  alexsubALTlem3  21610  tgpconcompeqg  21672  ghmcnp  21675  qustgplem  21681  blssps  21986  blss  21987  blcld  22067  metequiv2  22072  met2ndci  22084  prdsxmslem2  22091  txmetcnp  22109  nlmvscnlem1  22247  xrge0tsms  22392  ipcnlem1  22796  iscmet3  22843  cmetss  22865  minveclem3  22952  pmltpc  22970  ovolscalem2  23033  ovolicc2lem5  23040  ovolicc2  23041  nulmbl2  23055  ioombl1  23081  uniioombllem6  23106  uniioombl  23107  vitalilem3  23129  i1faddlem  23210  mbfmullem  23242  itg2const2  23258  itg2split  23266  lhop2  23526  dvfsumrlim  23542  itgsubst  23560  plydivex  23800  plyexmo  23816  ulmbdd  23900  cxploglim  24448  dchrptlem2  24734  lgsquad2lem2  24854  2sqlem5  24891  dchrvmasumif  24936  rpvmasum2  24945  dchrisum0re  24946  dchrisum0lem3  24952  dchrisum0  24953  dchrmusum  24957  dchrvmasum  24958  pntibndlem3  25025  pntlemp  25043  ostth3  25071  legtrid  25231  hlcgreu  25258  mirreu3  25294  opphllem  25372  oppperpex  25390  lnperpex  25440  trgcopy  25441  iscgra1  25447  cgraswap  25457  cgracom  25459  cgratr  25460  acopyeu  25470  ax5seglem9  25562  ax5seg  25563  axcontlem8  25596  axcontlem12  25600  wlkiswwlkfun  26038  wwlkextwrd  26049  usg2spthonot0  26209  frgranbnb  26340  frgrancvvdeqlemC  26359  ablo4  26581  smcnlem  26729  pjhthmo  27338  1stpreimas  28659  xrge0tsmsd  28909  locfinref  29029  xpinpreima2  29074  qqhval2  29147  dya2iocnrect  29463  orvcgteel  29649  orvclteel  29654  cnpcon  30259  txpcon  30261  conpcon  30264  pconpi1  30266  iccllyscon  30279  rellyscon  30280  cvmcov2  30304  cvmliftmolem2  30311  cvmliftmo  30313  cvmliftlem15  30327  cvmliftpht  30347  cvmlift3lem2  30349  cgrextend  31078  btwnouttr2  31092  btwnexch2  31093  cgrxfr  31125  lineext  31146  btwnconn1lem5  31161  btwnconn1lem13  31169  btwnconn3  31173  segletr  31184  segleantisym  31185  outsideofeq  31200  outsidele  31202  lineunray  31217  refssfne  31316  neibastop2lem  31318  neibastop2  31319  unblimceq0lem  31460  knoppndvlem22  31487  mblfinlem3  32401  mblfinlem4  32402  cnambfre  32411  itg2addnclem  32414  areacirclem5  32457  istotbnd3  32523  crngm4  32755  cvlcvr1  33427  4atlem12  33699  cdlemb  33881  paddasslem10  33916  paddasslem12  33918  paddasslem13  33919  lhpexle3lem  34098  cdlemd4  34289  cdlemefs32sn1aw  34503  cdleme43fsv1snlem  34509  cdleme32d  34533  cdleme32f  34535  cdleme40m  34556  cdleme40n  34557  cdleme50trn2  34640  cdlemftr3  34654  cdlemm10N  35208  dihvalcqpre  35325  dihopelvalcpre  35338  dihmeetlem1N  35380  dihglblem5apreN  35381  dihmeetlem4preN  35396  dihjat1lem  35518  mapd0  35755  mapdh9a  35880  mzpmfp  36111  mzpcompact2lem  36115  diophin  36137  pellexlem3  36196  pellex  36200  pell14qrmulcl  36228  jm2.19lem3  36359  jm2.25  36367  jm2.27b  36374  fnwe2lem2  36422  hbtlem2  36496  hbtlem5  36500  gsumws3  37304  gsumws4  37305  fnchoice  37994  stoweidlem53  38729  stoweidlem61  38737  qndenserrnbllem  38973  bgoldbtbnd  40009  upgrclwlkcompim  40969  wlkwwlkfun  41073  wwlksnextwrd  41084  2pthfrgr  41435  frgrnbnb  41444  frgrncvvdeqlemC  41459
  Copyright terms: Public domain W3C validator