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 483	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 725	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  disjxiun  5145  frpomin  6346  fsnex  7290  f1prex  7291  isotr  7341  weniso  7359  riota5f  7402  frxp2  8147  frxp3  8154  xpord3pred  8155  poseq  8161  fprlem2  8305  tfrlem9a  8405  oaass  8580  oeeui  8621  oaabs2  8668  coflton  8690  cofon1  8691  naddssim  8704  resixpfo  8953  omxpenlem  9096  pw2f1olem  9099  fopwdom  9103  fofinf1o  9351  marypha1lem  9456  ordiso2  9538  oismo  9563  ixpiunwdom  9613  cantnf  9716  ttrclss  9743  fseqenlem1  10047  iunfictbso  10137  dfac12lem2  10167  dfac12lem3  10168  infunsdom1  10236  infpssrlem5  10330  fin23lem24  10345  isf32lem2  10377  isf32lem4  10379  isf34lem4  10400  fin1a2lem12  10434  fin1a2lem13  10435  ttukeylem6  10537  fpwwe2lem11  10664  fpwwe2lem12  10665  fpwwe2  10666  winalim2  10719  wunex2  10761  tskord  10803  prlem934  11056  mulcmpblnr  11094  dedekind  11407  addrid  11424  cnegex  11425  negeu  11480  add20  11756  divdivdiv  11945  ltmul12a  12100  lemul12a  12102  lediv12a  12137  supaddc  12211  supmul1  12213  cru  12234  uzwo3  12957  xleadd1a  13264  xmullem  13275  xmulgt0  13294  xlemul1a  13299  ixxun  13372  ixxss12  13376  ioodisj  13491  fz0fzelfz0  13639  mulexpz  14099  rpexpmord  14164  leexp1a  14171  expmulnbnd  14229  hashf1  14450  fi1uzind  14490  brfi1indALT  14493  swrdccat  14717  reuccatpfxs1  14729  abs3lem  15317  rexanre  15325  cau3lem  15333  limsupgre  15457  limsupbnd2  15459  o1lo1  15513  rlimclim1  15521  rlimclim  15522  rlimcn1  15564  rlimcn3  15566  o1of2  15589  o1rlimmul  15595  lo1add  15603  lo1mul  15604  isercolllem1  15643  climcau  15649  caucvgrlem  15651  caucvgb  15658  summolem2  15694  summo  15695  modfsummod  15772  o1fsum  15791  prodmolem2  15911  addmodlteqALT  16301  rpdvds  16630  isprm5  16677  isprm6  16684  pclem  16806  pcqmul  16821  pcexp  16827  pcneg  16842  pcprmpw2  16850  pcadd  16857  pcmpt  16860  4sqlem13  16925  vdwlem2  16950  vdwlem7  16955  vdwlem12  16960  ramval  16976  ramub2  16982  ramz2  16992  ramcl  16997  cshwshashlem2  17065  imasval  17492  imasdsval  17496  mreexexd  17627  acsfn  17638  issubc3  17834  idfucl  17866  funcres2c  17889  isnat  17936  fucpropd  17968  xpcval  18167  xpcco  18173  prfval  18189  evlf2  18209  evlfcl  18213  curf12  18218  curf1cl  18219  curf2  18220  curfcl  18223  curf2ndf  18238  hof2val  18247  hofcl  18250  hofpropd  18258  yonedalem4a  18266  yonedainv  18272  drsdirfi  18296  pospo  18336  poslubmo  18402  posglbmo  18403  isipodrs  18528  acsinfd  18547  gsumvalx  18635  gsumpropd2lem  18638  mgmhmeql  18675  sgrppropd  18690  ismndd  18715  mndpropd  18718  mhmeql  18782  mndind  18784  frmdup3lem  18822  mhmmnd  19024  issubg4  19104  ssnmz  19125  conjnmzb  19211  f1otrspeq  19406  psgneu  19465  pgpfi  19564  sylow2blem3  19581  slwhash  19583  fislw  19584  sylow3lem2  19587  lsmdisj2  19641  pj1eu  19655  efgredlem  19706  frgpuplem  19731  gexex  19812  frgpnabl  19834  dprdfadd  19981  dpjidcl  20019  pgpfac1lem3  20038  pgpfaclem3  20044  ablfac2  20050  ablsimpgcygd  20067  ablsimpgfind  20071  ablsimpgprmd  20076  rngpropd  20118  ringpropd  20228  imadrhmcl  20689  islmhm2  20927  lmhmpropd  20962  lbsextlem4  21053  prmirredlem  21402  psgndiflemA  21537  lsmcss  21628  uvcf1  21730  frlmsslsp  21734  frlmup1  21736  assapropd  21809  psrval  21852  evlslem1  22035  mamucl  22331  mamuass  22332  mamudi  22333  mamudir  22334  mamuvs1  22335  mamuvs2  22336  mamulid  22373  mamurid  22374  dmatsubcl  22430  dmatmulcl  22432  scmatscm  22445  marrepval  22494  marepveval  22500  mdetunilem7  22550  gsummatr01lem4  22590  cpmatmcllem  22650  mat2pmatf1  22661  mat2pmatlin  22667  decpmatmul  22704  pm2mpmhmlem2  22751  chpidmat  22779  pptbas  22941  toponmre  23027  restbas  23092  iscncl  23203  cnrest2  23220  cnpdis  23227  lmcnp  23238  dishaus  23316  cmpcovf  23325  tgcmp  23335  dfconn2  23353  clsconn  23364  2ndcctbss  23389  dis2ndc  23394  1stccnp  23396  islly2  23418  cldllycmp  23429  locfincmp  23460  comppfsc  23466  kgentopon  23472  txcls  23538  ptpjopn  23546  dfac14  23552  xkoccn  23553  txcnp  23554  txcmpb  23578  txlm  23582  xkopt  23589  xkoco1cn  23591  xkoco2cn  23592  qtopcn  23648  qtoprest  23651  regr1lem2  23674  xkocnv  23748  qtophmeo  23751  fmfnfmlem4  23891  hausflim  23915  hauspwpwf1  23921  fclscmp  23964  alexsublem  23978  alexsubALTlem2  23982  alexsubALTlem3  23983  ptcmplem3  23988  ptcmplem4  23989  ptcmplem5  23990  cnextfun  23998  tmdgsum2  24030  symgtgp  24040  tsmsval2  24064  tsmsgsum  24073  utoptop  24169  ismet2  24269  blin  24357  metss2lem  24450  methaus  24459  met1stc  24460  met2ndci  24461  prdsxmslem2  24468  metcnp3  24479  metcnpi3  24485  metustto  24492  metustfbas  24496  nlmvscn  24634  nrginvrcn  24639  xrsxmet  24755  reconnlem1  24772  reconn  24774  xrge0tsms  24780  xmetdcn2  24783  metdscn  24802  addcnlem  24810  fsumcn  24818  cnheiborlem  24910  cnheibor  24911  bndth  24914  lebnum  24920  nmoleub2lem2  25073  ipcn  25204  iscmet3  25251  caubl  25266  rrxdstprj1  25367  minveclem3b  25386  minveclem7  25393  pjthlem2  25396  pmltpc  25409  volfiniun  25506  ioombl1  25521  dyadss  25553  dyaddisjlem  25554  dyadmax  25557  dyadmbllem  25558  opnmbllem  25560  itg1addlem2  25656  itg10a  25670  mbfi1fseqlem6  25680  itg2seq  25702  itg2monolem1  25710  itg2gt0  25720  itgfsum  25786  limcfval  25831  ellimc2  25836  ellimc3  25838  limcres  25845  limciun  25853  dvres  25870  dveflem  25941  rolle  25952  dvlip2  25958  c1liplem1  25959  dvgt0lem1  25965  dvgt0  25967  dvlt0  25968  dvne0  25974  dvfsumrlimge0  25995  ftc1lem6  26006  itgsubst  26014  mdegmullem  26044  ply1domn  26089  ply1divex  26102  fta1g  26134  fta1b  26136  plyf  26162  dgrlem  26193  coeid  26202  plydivalg  26264  aannenlem1  26293  aalioulem3  26299  aalioulem6  26302  abelthlem8  26406  efif1olem4  26509  chordthm  26799  xrlimcnp  26930  jensen  26951  lgamcvglem  27002  lgamcvg2  27017  sqf11  27101  fsumvma2  27177  perfectlem2  27193  lgsdilem  27287  lgsquad2lem2  27348  lgsquad3  27350  2sqlem5  27385  2sqlem9  27390  2sqb  27395  rpvmasumlem  27450  dchrisum0flb  27473  dchrisum0  27483  pntpbnd  27551  pntibndlem3  27555  pntleml  27574  nolt02o  27658  nosupbday  27668  nosupbnd2  27679  noinfbday  27683  noinfbnd2  27694  noetasuplem4  27699  noetainflem4  27703  noetalem1  27704  conway  27762  slerec  27782  sltlpss  27863  addsprop  27923  remulscllem2  28285  tgjustc1  28335  tgjustc2  28336  legov  28445  legtrid  28451  tglinethru  28496  tglnpt2  28501  tglineintmo  28502  mirreu3  28514  perpcom  28573  colperpexlem3  28592  mideu  28598  opphllem1  28607  hlpasch  28616  lnopp2hpgb  28623  trgcopy  28664  brcgr  28767  brbtwn2  28772  colinearalg  28777  axsegcon  28794  axeuclidlem  28829  axcontlem9  28839  ecgrtg  28850  elntg  28851  eengtrkg  28853  upgr1eopALT  28986  usgredg4  29086  subuhgr  29155  subumgr  29157  usgr2wspthon  29832  clwlkclwwlkf1  29876  eupth2lems  30104  n4cyclfrgr  30157  vacn  30560  blocni  30671  ubthlem3  30738  minvecolem7  30749  chocunii  31167  pjhthmo  31168  pjhthlem2  31258  kbass5  31986  mdsymlem5  32273  foresf1o  32357  fcobij  32561  xrofsup  32594  mgcoval  32770  mgcf1o  32787  xrge0tsmsd  32828  symgcntz  32865  archirngz  32954  archiabllem2a  32959  isarchiofld  33092  prmidl2  33219  smatrcl  33467  reff  33510  ordtconnlem1  33595  qqhval2  33653  volmeas  33920  fiunelcarsg  34006  ballotlemfc0  34182  ballotlemfcc  34183  signstfvneq0  34274  derangenlem  34851  erdsze2lem1  34883  pconnconn  34911  connpconn  34915  cvxsconn  34923  cvmliftmolem2  34962  cvmliftmo  34964  cvmlift2lem10  34992  cvmlift2lem12  34994  cvmlift3lem7  35005  mrsubff1  35194  msubff1  35236  ifscgr  35710  cgrxfr  35721  btwnconn1lem13  35765  btwnconn1lem14  35766  outsideofeq  35796  ellines  35818  finminlem  35872  fnejoin2  35923  unbdqndv2  36056  irrdiff  36875  poimirlem13  37176  poimirlem14  37177  poimirlem32  37195  opnmbllem0  37199  mblfinlem3  37202  itg2addnclem  37214  itg2addnc  37217  ftc1cnnc  37235  upixp  37272  filbcmb  37283  sstotbnd2  37317  isbnd3  37327  prdsbnd2  37338  cntotbnd  37339  ismtyima  37346  bfp  37367  rrncmslem  37375  unichnidl  37574  lshpcmp  38529  islshpat  38558  lfl0f  38610  ishlat3N  38895  3dim1  39009  islvol5  39121  lvoli2  39123  lncvrelatN  39323  pclfinclN  39492  pexmidlem8N  39519  idltrn  39692  cdleme42keg  40028  cdleme42mgN  40030  cdlemf2  40104  cdlemg2cex  40133  trlcoat  40265  dihopelvalcpre  40790  dih1dimatlem  40871  dihjatcclem4  40963  lcfl7N  41043  lcfrlem9  41092  mapdh9a  41331  hdmapglem7  41471  aks4d1p8  41627  isprimroot  41633  evl1gprodd  41657  sticksstones11  41697  imacrhmcl  41819  fsuppind  41888  fsuppssind  41891  mhpind  41892  renegeulemv  41988  sn-subeu  42046  remulinvcom  42052  sn-itrere  42086  sn-retire  42087  prjspertr  42094  prjspreln0  42098  flt4lem7  42148  nna4b4nsq  42149  nacsfix  42197  mzpsubst  42233  mzpcompact2lem  42236  eldioph2lem2  42246  eldioph2  42247  eldioph2b  42248  diophin  42257  diophun  42258  irrapxlem3  42309  irrapxlem5  42311  pell1234qrreccl  42339  pell1234qrmulcl  42340  pell14qrdich  42354  pell1qrge1  42355  pell1qrgaplem  42358  monotuz  42427  acongtr  42464  acongrep  42466  jm2.23  42482  jm2.26a  42486  jm2.26lem3  42487  jm2.26  42488  jm2.27  42494  wepwsolem  42531  fnwe2lem2  42540  kelac1  42552  kercvrlsm  42572  hbtlem5  42617  hbt  42619  mpaaeu  42639  cantnfresb  42818  onmcl  42825  tfsconcatun  42831  tfsconcatfn  42832  tfsconcatfv1  42833  tfsconcatfv2  42834  naddcnff  42856  rfovcnvf1od  43499  mnurndlem1  43783  cncmpmax  44459  rfcnnnub  44463  disjxp1  44498  iccintsng  44971  fprodcn  45051  lptioo2  45082  lptioo1  45083  limclner  45102  stoweidlem31  45482  stoweidlem34  45485  stoweidlem35  45486  stoweidlem49  45500  stoweidlem59  45510  stoweidlem62  45513  fourierdlem60  45617  fourierdlem61  45618  fourierdlem87  45644  iundjiun  45911  ismeannd  45918  hoidmvle  46051  smfsuplem2  46263  2reu8i  46556  prproropf1olem2  46907  paireqne  46914  perfectALTVlem2  47125  mogoldbb  47188  bgoldbtbndlem2  47209  bgoldbtbndlem3  47210  uspgrimprop  47283  mndpsuppss  47547  scmsuppss  47548  lindslinindsimp2lem5  47642  elfzolborelfzop1  47699  elbigolo1  47742  itschlc0xyqsol1  47951  itschlc0xyqsol  47952  iccdisj  48029  toslat  48105  functhinclem4  48162