Theorem simprrr 781

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 484	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	ad2antll 729	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  prproe  4869  f1prex  7259  fliftfun  7287  fprresex  8289  nnaordex2  8603  naddssim  8649  mapdom2  9112  domunfican  9272  fofinf1o  9283  finsschain  9310  wemaplem3  9501  oemapvali  9637  iunfictbso  10067  enfin2i  10274  fin1a2s  10367  distrlem4pr  10979  mulcmpblnr  11024  prsrlem1  11025  addsrmo  11026  mulsrmo  11027  divdivdiv  11883  divsubdiv  11898  lediv12a  12076  xralrple  13165  seqcaopr  14004  leexp2r  14139  hashbclem  14417  wrd2ind  14688  cshwidxmod  14768  rtrclreclem4  15027  relexpindlem  15029  rtrclind  15031  rlimresb  15531  summo  15683  fsum2dlem  15736  prodmo  15902  fprod2dlem  15946  bezoutlem3  16511  bezoutlem4  16512  qredeu  16628  coprmproddvdslem  16632  prmdvdsncoprmbd  16697  pcqmul  16824  pcadd  16860  pockthg  16877  ramub1lem2  16998  cshwsdisj  17069  mreexexlem4d  17608  issubc3  17811  cofucl  17850  setcmon  18049  setcepi  18050  drsdirfi  18266  poslubmo  18370  posglbmo  18371  grprida  18602  ghmpreima  19170  gaorber  19240  psgnunilem4  19427  psgneu  19436  odcau  19534  pgpssslw  19544  fislw  19555  lsmsubm  19583  efgsfo  19669  pgpfac1  20012  pgpfaclem2  20014  pgpfaclem3  20015  unitgrp  20292  islmodd  20772  lmodprop2d  20830  lsspropd  20924  lbsextlem4  21071  assapropd  21781  evlslem1  21989  mdetunilem8  22506  mdetmul  22510  ppttop  22894  epttop  22896  restbas  23045  iscnp4  23150  cnpco  23154  nrmsep  23244  regsep2  23263  ordthauslem  23270  1stcfb  23332  2ndcctbss  23342  2ndcdisj  23343  2ndcomap  23345  dis2ndc  23347  1stcelcls  23348  nlly2i  23363  islly2  23371  hausllycmp  23381  lly1stc  23383  comppfsc  23419  1stckgenlem  23440  ptbasin  23464  txcls  23491  ptcnp  23509  txlly  23523  txnlly  23524  txtube  23527  txcmplem1  23528  txcmplem2  23529  xkococnlem  23546  basqtop  23598  regr1lem  23626  kqreglem1  23628  kqreglem2  23629  kqnrmlem1  23630  kqnrmlem2  23631  reghmph  23680  nrmhmph  23681  filuni  23772  rnelfmlem  23839  fmufil  23846  fclscf  23912  fclsfnflim  23914  flimfnfcls  23915  uffclsflim  23918  cnpfcfi  23927  cnpfcf  23928  alexsublem  23931  alexsubALTlem3  23936  tgpconncompeqg  23999  ghmcnp  24002  qustgplem  24008  blssps  24312  blss  24313  blcld  24393  metequiv2  24398  met2ndci  24410  prdsxmslem2  24417  txmetcnp  24435  nlmvscnlem1  24574  xrge0tsms  24723  ipcnlem1  25145  iscmet3  25193  metsscmetcld  25215  minveclem3  25329  pmltpc  25351  ovolscalem2  25415  ovolicc2lem5  25422  ovolicc2  25423  nulmbl2  25437  ioombl1  25463  uniioombllem6  25489  uniioombl  25490  vitalilem3  25511  i1faddlem  25594  mbfmullem  25626  itg2const2  25642  itg2split  25650  lhop2  25920  dvfsumrlim  25938  itgsubst  25956  plydivex  26205  plyexmo  26221  ulmbdd  26307  cxploglim  26888  dchrptlem2  27176  lgsquad2lem2  27296  2sqlem5  27333  dchrvmasumif  27414  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lem3  27430  dchrisum0  27431  dchrmusum  27435  dchrvmasum  27436  pntibndlem3  27503  pntlemp  27521  ostth3  27549  nosupbday  27617  nosupbnd1lem1  27620  nosupbnd2  27628  noinfbday  27632  noinfbnd1lem1  27635  noinfbnd2  27643  conway  27711  madebdaylemlrcut  27810  mulsproplem9  28027  mulsuniflem  28052  uzsind  28293  readdscl  28350  legtrid  28518  hlcgreu  28545  mirreu3  28581  opphllem  28662  oppperpex  28680  lnperpex  28730  trgcopy  28731  iscgra1  28737  cgraswap  28747  cgracom  28749  cgratr  28750  flatcgra  28751  acopyeu  28761  ax5seglem9  28864  ax5seg  28865  axcontlem8  28898  axcontlem12  28902  upgrclwlkcompim  29711  wwlksnextwrd  29827  2pthfrgr  30213  frgrnbnb  30222  ablo4  30479  smcnlem  30626  pjhthmo  31231  1stpreimas  32629  xrge0tsmsd  33002  locfinref  33831  xpinpreima2  33897  qqhval2  33972  dya2iocnrect  34272  orvcgteel  34459  orvclteel  34464  cnpconn  35217  txpconn  35219  connpconn  35222  pconnpi1  35224  iccllysconn  35237  rellysconn  35238  cvmcov2  35262  cvmliftmolem2  35269  cvmliftmo  35271  cvmliftlem15  35285  cvmliftpht  35305  cvmlift3lem2  35307  cgrextend  35996  btwnouttr2  36010  btwnexch2  36011  cgrxfr  36043  lineext  36064  btwnconn1lem5  36079  btwnconn1lem13  36087  btwnconn3  36091  segletr  36102  segleantisym  36103  outsideofeq  36118  outsidele  36120  lineunray  36135  refssfne  36346  neibastop2lem  36348  neibastop2  36349  weiunpo  36453  unblimceq0lem  36494  knoppndvlem22  36521  mblfinlem3  37653  mblfinlem4  37654  cnambfre  37662  itg2addnclem  37665  areacirclem5  37706  istotbnd3  37765  crngm4  37997  cvlcvr1  39332  4atlem12  39606  cdlemb  39788  paddasslem10  39823  paddasslem12  39825  paddasslem13  39826  lhpexle3lem  40005  cdlemd4  40195  cdlemefs32sn1aw  40408  cdleme43fsv1snlem  40414  cdleme32d  40438  cdleme32f  40440  cdleme40m  40461  cdleme40n  40462  cdleme50trn2  40545  cdlemftr3  40559  cdlemm10N  41112  dihvalcqpre  41229  dihopelvalcpre  41242  dihmeetlem1N  41284  dihglblem5apreN  41285  dihmeetlem4preN  41300  dihjat1lem  41422  mapd0  41659  mapdh9a  41783  nna4b4nsq  42648  mzpmfp  42735  mzpcompact2lem  42739  diophin  42760  pellexlem3  42819  pellex  42823  pell14qrmulcl  42851  jm2.19lem3  42980  jm2.25  42988  jm2.27b  42995  fnwe2lem2  43040  hbtlem2  43113  hbtlem5  43117  gsumws3  44185  gsumws4  44186  mnuprdlem1  44261  mnuprdlem2  44262  mnuprdlem4  44264  fnchoice  45023  stoweidlem53  46051  stoweidlem61  46059  qndenserrnbllem  46292  bgoldbtbnd  47810  cycldlenngric  47928  grtrimap  47947  isubgr3stgrlem6  47970  prsthinc  49453