Theorem simprrr 794

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprrr	⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

Proof of Theorem simprrr

Step	Hyp	Ref	Expression
1		simpr 490	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	ad2antll 742	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  prproe  4868  f1prex  7288  fliftfun  7316  fprresex  8312  nnaordex2  8630  naddssim  8677  mapdom2  9149  domunfican  9294  fofinf1o  9302  finsschain  9329  wemaplem3  9523  oemapvali  9666  iunfictbso  10120  enfin2i  10326  fin1a2s  10419  distrlem4pr  11038  mulcmpblnr  11083  prsrlem1  11084  addsrmo  11085  mulsrmo  11086  divdivdiv  11943  divsubdiv  11958  lediv12a  12135  xralrple  13259  seqcaopr  14105  leexp2r  14240  hashbclem  14519  wrd2ind  14794  cshwidxmod  14876  rtrclreclem4  15136  relexpindlem  15138  rtrclind  15140  rlimresb  15654  summo  15805  fsum2dlem  15858  prodmo  16027  fprod2dlem  16071  bezoutlem3  16635  bezoutlem4  16636  qredeu  16752  coprmproddvdslem  16756  prmdvdsncoprmbd  16822  pcqmul  16949  pcadd  16985  pockthg  17002  ramub1lem2  17123  cshwsdisj  17194  mreexexlem4d  17739  issubc3  17942  cofucl  17981  setcmon  18180  setcepi  18181  drsdirfi  18397  poslubmo  18501  posglbmo  18502  mgmn0plusgf  18745  grprida  18773  ghmpreima  19366  gaorber  19436  psgnunilem4  19625  psgneu  19634  odcau  19732  pgpssslw  19742  fislw  19753  lsmsubm  19781  efgsfo  19867  pgpfac1  20210  pgpfaclem2  20212  pgpfaclem3  20213  unitgrp  20525  islmodd  21051  lmodprop2d  21109  lsspropd  21202  lbsextlem4  21349  assapropd  22087  evlslem1  22299  mdetunilem8  22842  mdetmul  22846  ppttop  23233  epttop  23235  restbas  23384  iscnp4  23489  cnpco  23493  nrmsep  23583  regsep2  23602  ordthauslem  23609  1stcfb  23671  2ndcctbss  23682  2ndcdisj  23683  2ndcomap  23685  dis2ndc  23687  1stcelcls  23688  nlly2i  23703  islly2  23711  hausllycmp  23721  lly1stc  23723  comppfsc  23759  1stckgenlem  23780  ptbasin  23804  txcls  23831  ptcnp  23849  txlly  23863  txnlly  23864  txtube  23867  txcmplem1  23868  txcmplem2  23869  xkococnlem  23886  basqtop  23938  regr1lem  23966  kqreglem1  23968  kqreglem2  23969  kqnrmlem1  23970  kqnrmlem2  23971  reghmph  24020  nrmhmph  24021  filuni  24112  rnelfmlem  24179  fmufil  24186  fclscf  24252  fclsfnflim  24254  flimfnfcls  24255  uffclsflim  24258  cnpfcfi  24267  cnpfcf  24268  alexsublem  24271  alexsubALTlem3  24276  tgpconncompeqg  24339  ghmcnp  24342  qustgplem  24348  blssps  24651  blss  24652  blcld  24732  metequiv2  24737  met2ndci  24749  prdsxmslem2  24756  txmetcnp  24774  nlmvscnlem1  24913  xrge0tsms  25062  ipcnlem1  25474  iscmet3  25522  metsscmetcld  25544  minveclem3  25658  pmltpc  25679  ovolscalem2  25743  ovolicc2lem5  25750  ovolicc2  25751  nulmbl2  25765  ioombl1  25791  uniioombllem6  25817  uniioombl  25818  vitalilem3  25839  i1faddlem  25922  mbfmullem  25954  itg2const2  25970  itg2split  25978  lhop2  26244  dvfsumrlim  26260  itgsubst  26278  plydivex  26528  plyexmo  26544  ulmbdd  26631  cxploglim  27212  dchrptlem2  27499  lgsquad2lem2  27619  2sqlem5  27656  dchrvmasumif  27737  rpvmasum2  27746  dchrisum0re  27747  dchrisum0lem3  27753  dchrisum0  27754  dchrmusum  27758  dchrvmasum  27759  pntibndlem3  27826  pntlemp  27844  ostth3  27872  nosupbday  27939  nosupbnd1lem1  27942  nosupbnd2  27950  noinfbday  27954  noinfbnd1lem1  27957  noinfbnd2  27965  conway  28042  madebdaylemlrcut  28162  mulsproplem9  28387  mulsuniflem  28412  uzsind  28668  bdayfinbndlem1  28730  readdscl  28762  legtrid  28931  hlcgreu  28961  mirreu3  29003  opphllem  29088  oppperpex  29106  lnperpex  29186  trgcopy  29188  iscgra1  29194  cgraswap  29204  cgracom  29206  cgratr  29207  flatcgra  29209  acopyeu  29219  ax5seglem9  29380  ax5seg  29381  axcontlem8  29414  axcontlem12  29418  upgrclwlkcompim  30233  wwlksnextwrd  30351  2pthfrgr  30750  frgrnbnb  30759  ablo4  31017  smcnlem  31164  pjhthmo  31769  1stpreimas  33165  xrge0tsmsd  33500  locfinref  34338  xpinpreima2  34404  qqhval2  34479  dya2iocnrect  34779  orvcgteel  34966  orvclteel  34971  cnpconn  35796  txpconn  35798  connpconn  35801  pconnpi1  35803  iccllysconn  35816  rellysconn  35817  cvmcov2  35841  cvmliftmolem2  35848  cvmliftmo  35850  cvmliftlem15  35864  cvmliftpht  35884  cvmlift3lem2  35886  cgrextend  36575  btwnouttr2  36589  btwnexch2  36590  cgrxfr  36622  lineext  36643  btwnconn1lem5  36658  btwnconn1lem13  36666  btwnconn3  36670  segletr  36681  segleantisym  36682  outsideofeq  36697  outsidele  36699  lineunray  36714  refssfne  36964  neibastop2lem  36966  neibastop2  36967  weiunpo  37071  unblimceq0lem  37190  knoppndvlem22  37217  mblfinlem3  38395  mblfinlem4  38396  cnambfre  38404  itg2addnclem  38407  areacirclem5  38448  istotbnd3  38508  crngm4  38740  cvlcvr1  40199  4atlem12  40472  cdlemb  40654  paddasslem10  40689  paddasslem12  40691  paddasslem13  40692  lhpexle3lem  40871  cdlemd4  41061  cdlemefs32sn1aw  41274  cdleme43fsv1snlem  41280  cdleme32d  41304  cdleme32f  41306  cdleme40m  41327  cdleme40n  41328  cdleme50trn2  41411  cdlemftr3  41425  cdlemm10N  41978  dihvalcqpre  42095  dihopelvalcpre  42108  dihmeetlem1N  42150  dihglblem5apreN  42151  dihmeetlem4preN  42166  dihjat1lem  42288  mapd0  42525  mapdh9a  42649  nna4b4nsq  43493  mzpmfp  43579  mzpcompact2lem  43583  diophin  43604  pellexlem3  43659  pellex  43663  pell14qrmulcl  43691  jm2.19lem3  43819  jm2.25  43827  jm2.27b  43834  fnwe2lem2  43879  hbtlem2  43952  hbtlem5  43956  gsumws3  45023  gsumws4  45024  mnuprdlem1  45083  mnuprdlem2  45084  mnuprdlem4  45086  fnchoice  45850  stoweidlem53  46868  stoweidlem61  46876  qndenserrnbllem  47109  bgoldbtbnd  48712  cycldlenngric  48831  grtrimap  48851  isubgr3stgrlem6  48874  prsthinc  50377