Theorem simplrr 776

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

Assertion

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

Proof of Theorem simplrr

Step	Hyp	Ref	Expression
1		simpr 487	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 725	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  disjxiun  5054  fsnex  7031  f1prex  7032  isotr  7081  weniso  7099  riota5f  7134  tfrlem9a  8014  oaass  8179  oeeui  8220  oaabs2  8264  resixpfo  8492  omxpenlem  8610  pw2f1olem  8613  fopwdom  8617  fofinf1o  8791  marypha1lem  8889  ordiso2  8971  oismo  8996  ixpiunwdom  9047  cantnf  9148  fseqenlem1  9442  iunfictbso  9532  dfac12lem2  9562  dfac12lem3  9563  infunsdom1  9627  infpssrlem5  9721  fin23lem24  9736  isf32lem2  9768  isf32lem4  9770  isf34lem4  9791  fin1a2lem12  9825  fin1a2lem13  9826  ttukeylem6  9928  fpwwe2lem12  10055  fpwwe2lem13  10056  fpwwe2  10057  winalim2  10110  wunex2  10152  tskord  10194  prlem934  10447  mulcmpblnr  10485  dedekind  10795  addid1  10812  cnegex  10813  negeu  10868  add20  11144  divdivdiv  11333  ltmul12a  11488  lemul12a  11490  lediv12a  11525  supaddc  11600  supmul1  11602  cru  11622  uzwo3  12335  xleadd1a  12638  xmullem  12649  xmulgt0  12668  xlemul1a  12673  ixxun  12746  ixxss12  12750  ioodisj  12860  fz0fzelfz0  13005  mulexpz  13461  rpexpmord  13524  leexp1a  13531  expmulnbnd  13588  hashf1  13807  fi1uzind  13847  brfi1indALT  13850  swrdccat  14089  reuccatpfxs1  14101  abs3lem  14690  rexanre  14698  cau3lem  14706  limsupgre  14830  limsupbnd2  14832  o1lo1  14886  rlimclim1  14894  rlimclim  14895  rlimcn1  14937  rlimcn2  14939  o1of2  14961  o1rlimmul  14967  lo1add  14975  lo1mul  14976  isercolllem1  15013  climcau  15019  caucvgrlem  15021  caucvgb  15028  summolem2  15065  summo  15066  modfsummod  15141  o1fsum  15160  prodmolem2  15281  addmodlteqALT  15667  rpdvds  15996  isprm5  16043  isprm6  16050  pclem  16167  pcqmul  16182  pcexp  16188  pcneg  16202  pcprmpw2  16210  pcadd  16217  pcmpt  16220  4sqlem13  16285  vdwlem2  16310  vdwlem7  16315  vdwlem12  16320  ramval  16336  ramub2  16342  ramz2  16352  ramcl  16357  cshwshashlem2  16422  imasval  16776  imasdsval  16780  mreexexd  16911  acsfn  16922  issubc3  17111  idfucl  17143  funcres2c  17163  isnat  17209  fucpropd  17239  xpcval  17419  xpcco  17425  prfval  17441  evlf2  17460  evlfcl  17464  curf12  17469  curf1cl  17470  curf2  17471  curfcl  17474  curf2ndf  17489  hof2val  17498  hofcl  17501  hofpropd  17509  yonedalem4a  17517  yonedainv  17523  drsdirfi  17540  pospo  17575  poslubmo  17748  posglbmo  17749  isipodrs  17763  acsinfd  17782  gsumvalx  17878  gsumpropd2lem  17881  ismndd  17925  mndpropd  17928  mhmeql  17982  mndind  17984  frmdup3lem  18023  mhmmnd  18213  issubg4  18290  ssnmz  18310  conjnmzb  18385  f1otrspeq  18567  psgneu  18626  pgpfi  18722  sylow2blem3  18739  slwhash  18741  fislw  18742  sylow3lem2  18745  lsmdisj2  18800  pj1eu  18814  efgredlem  18865  frgpuplem  18890  gexex  18965  frgpnabl  18987  dprdfadd  19134  dpjidcl  19172  pgpfac1lem3  19191  pgpfaclem3  19197  ablfac2  19203  ablsimpgcygd  19220  ablsimpgfind  19224  ablsimpgprmd  19229  ringpropd  19324  islmhm2  19802  lmhmpropd  19837  lbsextlem4  19925  assapropd  20093  psrval  20134  evlslem1  20287  prmirredlem  20632  psgndiflemA  20737  lsmcss  20828  uvcf1  20928  frlmsslsp  20932  frlmup1  20934  mamucl  21002  mamuass  21003  mamudi  21004  mamudir  21005  mamuvs1  21006  mamuvs2  21007  mamulid  21042  mamurid  21043  dmatsubcl  21099  dmatmulcl  21101  scmatscm  21114  marrepval  21163  marepveval  21169  mdetunilem7  21219  gsummatr01lem4  21259  cpmatmcllem  21318  mat2pmatf1  21329  mat2pmatlin  21335  decpmatmul  21372  pm2mpmhmlem2  21419  chpidmat  21447  pptbas  21608  toponmre  21693  restbas  21758  iscncl  21869  cnrest2  21886  cnpdis  21893  lmcnp  21904  dishaus  21982  cmpcovf  21991  tgcmp  22001  dfconn2  22019  clsconn  22030  2ndcctbss  22055  dis2ndc  22060  1stccnp  22062  islly2  22084  cldllycmp  22095  locfincmp  22126  comppfsc  22132  kgentopon  22138  txcls  22204  ptpjopn  22212  dfac14  22218  xkoccn  22219  txcnp  22220  txcmpb  22244  txlm  22248  xkopt  22255  xkoco1cn  22257  xkoco2cn  22258  qtopcn  22314  qtoprest  22317  regr1lem2  22340  xkocnv  22414  qtophmeo  22417  fmfnfmlem4  22557  hausflim  22581  hauspwpwf1  22587  fclscmp  22630  alexsublem  22644  alexsubALTlem2  22648  alexsubALTlem3  22649  ptcmplem3  22654  ptcmplem4  22655  ptcmplem5  22656  cnextfun  22664  tmdgsum2  22696  symgtgp  22706  tsmsval2  22730  tsmsgsum  22739  utoptop  22835  ismet2  22935  blin  23023  metss2lem  23113  methaus  23122  met1stc  23123  met2ndci  23124  prdsxmslem2  23131  metcnp3  23142  metcnpi3  23148  metustto  23155  metustfbas  23159  nlmvscn  23288  nrginvrcn  23293  xrsxmet  23409  reconnlem1  23426  reconn  23428  xrge0tsms  23434  xmetdcn2  23437  metdscn  23456  addcnlem  23464  fsumcn  23470  cnheiborlem  23550  cnheibor  23551  bndth  23554  lebnum  23560  nmoleub2lem2  23712  ipcn  23841  iscmet3  23888  caubl  23903  rrxdstprj1  24004  minveclem3b  24023  minveclem7  24030  pjthlem2  24033  pmltpc  24043  volfiniun  24140  ioombl1  24155  dyadss  24187  dyaddisjlem  24188  dyadmax  24191  dyadmbllem  24192  opnmbllem  24194  itg1addlem2  24290  itg10a  24303  mbfi1fseqlem6  24313  itg2seq  24335  itg2monolem1  24343  itg2gt0  24353  itgfsum  24419  limcfval  24462  ellimc2  24467  ellimc3  24469  limcres  24476  limciun  24484  dvres  24501  dveflem  24568  rolle  24579  dvlip2  24584  c1liplem1  24585  dvgt0lem1  24591  dvgt0  24593  dvlt0  24594  dvne0  24600  dvfsumrlimge0  24619  ftc1lem6  24630  itgsubst  24638  mdegmullem  24664  ply1domn  24709  ply1divex  24722  fta1g  24753  fta1b  24755  plyf  24780  dgrlem  24811  coeid  24820  plydivalg  24880  aannenlem1  24909  aalioulem3  24915  aalioulem6  24918  abelthlem8  25019  efif1olem4  25121  chordthm  25407  xrlimcnp  25538  jensen  25558  lgamcvglem  25609  lgamcvg2  25624  sqf11  25708  fsumvma2  25782  perfectlem2  25798  lgsdilem  25892  lgsquad2lem2  25953  lgsquad3  25955  2sqlem5  25990  2sqlem9  25995  2sqb  26000  rpvmasumlem  26055  dchrisum0flb  26078  dchrisum0  26088  pntpbnd  26156  pntibndlem3  26160  pntleml  26179  tgjustc1  26253  tgjustc2  26254  legov  26363  legtrid  26369  tglinethru  26414  tglnpt2  26419  tglineintmo  26420  mirreu3  26432  perpcom  26491  colperpexlem3  26510  mideu  26516  opphllem1  26525  hlpasch  26534  lnopp2hpgb  26541  trgcopy  26582  brcgr  26678  brbtwn2  26683  colinearalg  26688  axsegcon  26705  axeuclidlem  26740  axcontlem9  26750  ecgrtg  26761  elntg  26762  eengtrkg  26764  upgr1eopALT  26894  usgredg4  26991  subuhgr  27060  subumgr  27062  usgr2wspthon  27736  clwlkclwwlkf1  27780  eupth2lems  28009  n4cyclfrgr  28062  vacn  28463  blocni  28574  ubthlem3  28641  minvecolem7  28652  chocunii  29070  pjhthmo  29071  pjhthlem2  29161  kbass5  29889  mdsymlem5  30176  foresf1o  30257  fcobij  30450  xrofsup  30484  xrge0tsmsd  30685  symgcntz  30722  archirngz  30811  archiabllem2a  30816  isarchiofld  30883  prmidl2  30951  smatrcl  31054  reff  31096  ordtconnlem1  31160  qqhval2  31216  volmeas  31483  fiunelcarsg  31567  ballotlemfc0  31743  ballotlemfcc  31744  signstfvneq0  31835  derangenlem  32411  erdsze2lem1  32443  pconnconn  32471  connpconn  32475  cvxsconn  32483  cvmliftmolem2  32522  cvmliftmo  32524  cvmlift2lem10  32552  cvmlift2lem12  32554  cvmlift3lem7  32565  mrsubff1  32754  msubff1  32796  frpomin  33071  poseq  33088  fprlem2  33131  nolt02o  33192  noprefixmo  33195  nosupbnd2  33209  noetalem3  33212  noetalem5  33214  conway  33257  slerec  33270  ifscgr  33498  cgrxfr  33509  btwnconn1lem13  33553  btwnconn1lem14  33554  outsideofeq  33584  ellines  33606  finminlem  33659  fnejoin2  33710  unbdqndv2  33843  poimirlem13  34897  poimirlem14  34898  poimirlem32  34916  opnmbllem0  34920  mblfinlem3  34923  itg2addnclem  34935  itg2addnc  34938  ftc1cnnc  34958  upixp  34996  filbcmb  35007  sstotbnd2  35044  isbnd3  35054  prdsbnd2  35065  cntotbnd  35066  ismtyima  35073  bfp  35094  rrncmslem  35102  unichnidl  35301  lshpcmp  36116  islshpat  36145  lfl0f  36197  ishlat3N  36482  3dim1  36595  islvol5  36707  lvoli2  36709  lncvrelatN  36909  pclfinclN  37078  pexmidlem8N  37105  idltrn  37278  cdleme42keg  37614  cdleme42mgN  37616  cdlemf2  37690  cdlemg2cex  37719  trlcoat  37851  dihopelvalcpre  38376  dih1dimatlem  38457  dihjatcclem4  38549  lcfl7N  38629  lcfrlem9  38678  mapdh9a  38917  hdmapglem7  39057  renegeulemv  39188  remulinvcom  39238  prjspertr  39245  prjspreln0  39249  nacsfix  39299  mzpsubst  39335  mzpcompact2lem  39338  eldioph2lem2  39348  eldioph2  39349  eldioph2b  39350  diophin  39359  diophun  39360  irrapxlem3  39411  irrapxlem5  39413  pell1234qrreccl  39441  pell1234qrmulcl  39442  pell14qrdich  39456  pell1qrge1  39457  pell1qrgaplem  39460  monotuz  39528  acongtr  39565  acongrep  39567  jm2.23  39583  jm2.26a  39587  jm2.26lem3  39588  jm2.26  39589  jm2.27  39595  wepwsolem  39632  fnwe2lem2  39641  kelac1  39653  kercvrlsm  39673  hbtlem5  39718  hbt  39720  mpaaeu  39740  rfovcnvf1od  40340  mnurndlem1  40607  cncmpmax  41279  rfcnnnub  41283  disjxp1  41321  iccintsng  41788  fprodcn  41870  lptioo2  41901  lptioo1  41902  limclner  41921  stoweidlem31  42306  stoweidlem34  42309  stoweidlem35  42310  stoweidlem49  42324  stoweidlem59  42334  stoweidlem62  42337  fourierdlem60  42441  fourierdlem61  42442  fourierdlem87  42468  iundjiun  42732  ismeannd  42739  hoidmvle  42872  smfsuplem2  43076  2reu8i  43302  prproropf1olem2  43656  paireqne  43663  perfectALTVlem2  43877  mogoldbb  43940  bgoldbtbndlem2  43961  bgoldbtbndlem3  43962  isomgrtrlem  43993  mgmhmeql  44060  mndpsuppss  44409  scmsuppss  44410  lindslinindsimp2lem5  44507  elfzolborelfzop1  44564  elbigolo1  44607  itschlc0xyqsol1  44743  itschlc0xyqsol  44744