Theorem simplrr 774

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 723	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  5144  frpomin  6340  fsnex  7283  f1prex  7284  isotr  7335  weniso  7353  riota5f  7396  frxp2  8132  frxp3  8139  xpord3pred  8140  poseq  8146  fprlem2  8288  tfrlem9a  8388  oaass  8563  oeeui  8604  oaabs2  8650  coflton  8672  cofon1  8673  naddssim  8686  resixpfo  8932  omxpenlem  9075  pw2f1olem  9078  fopwdom  9082  fofinf1o  9329  marypha1lem  9430  ordiso2  9512  oismo  9537  ixpiunwdom  9587  cantnf  9690  ttrclss  9717  fseqenlem1  10021  iunfictbso  10111  dfac12lem2  10141  dfac12lem3  10142  infunsdom1  10210  infpssrlem5  10304  fin23lem24  10319  isf32lem2  10351  isf32lem4  10353  isf34lem4  10374  fin1a2lem12  10408  fin1a2lem13  10409  ttukeylem6  10511  fpwwe2lem11  10638  fpwwe2lem12  10639  fpwwe2  10640  winalim2  10693  wunex2  10735  tskord  10777  prlem934  11030  mulcmpblnr  11068  dedekind  11381  addrid  11398  cnegex  11399  negeu  11454  add20  11730  divdivdiv  11919  ltmul12a  12074  lemul12a  12076  lediv12a  12111  supaddc  12185  supmul1  12187  cru  12208  uzwo3  12931  xleadd1a  13236  xmullem  13247  xmulgt0  13266  xlemul1a  13271  ixxun  13344  ixxss12  13348  ioodisj  13463  fz0fzelfz0  13611  mulexpz  14072  rpexpmord  14137  leexp1a  14144  expmulnbnd  14202  hashf1  14422  fi1uzind  14462  brfi1indALT  14465  swrdccat  14689  reuccatpfxs1  14701  abs3lem  15289  rexanre  15297  cau3lem  15305  limsupgre  15429  limsupbnd2  15431  o1lo1  15485  rlimclim1  15493  rlimclim  15494  rlimcn1  15536  rlimcn3  15538  o1of2  15561  o1rlimmul  15567  lo1add  15575  lo1mul  15576  isercolllem1  15615  climcau  15621  caucvgrlem  15623  caucvgb  15630  summolem2  15666  summo  15667  modfsummod  15744  o1fsum  15763  prodmolem2  15883  addmodlteqALT  16272  rpdvds  16601  isprm5  16648  isprm6  16655  pclem  16775  pcqmul  16790  pcexp  16796  pcneg  16811  pcprmpw2  16819  pcadd  16826  pcmpt  16829  4sqlem13  16894  vdwlem2  16919  vdwlem7  16924  vdwlem12  16929  ramval  16945  ramub2  16951  ramz2  16961  ramcl  16966  cshwshashlem2  17034  imasval  17461  imasdsval  17465  mreexexd  17596  acsfn  17607  issubc3  17803  idfucl  17835  funcres2c  17856  isnat  17902  fucpropd  17934  xpcval  18133  xpcco  18139  prfval  18155  evlf2  18175  evlfcl  18179  curf12  18184  curf1cl  18185  curf2  18186  curfcl  18189  curf2ndf  18204  hof2val  18213  hofcl  18216  hofpropd  18224  yonedalem4a  18232  yonedainv  18238  drsdirfi  18262  pospo  18302  poslubmo  18368  posglbmo  18369  isipodrs  18494  acsinfd  18513  gsumvalx  18601  gsumpropd2lem  18604  mgmhmeql  18641  sgrppropd  18656  ismndd  18681  mndpropd  18684  mhmeql  18743  mndind  18745  frmdup3lem  18783  mhmmnd  18983  issubg4  19061  ssnmz  19082  conjnmzb  19167  f1otrspeq  19356  psgneu  19415  pgpfi  19514  sylow2blem3  19531  slwhash  19533  fislw  19534  sylow3lem2  19537  lsmdisj2  19591  pj1eu  19605  efgredlem  19656  frgpuplem  19681  gexex  19762  frgpnabl  19784  dprdfadd  19931  dpjidcl  19969  pgpfac1lem3  19988  pgpfaclem3  19994  ablfac2  20000  ablsimpgcygd  20017  ablsimpgfind  20021  ablsimpgprmd  20026  rngpropd  20068  ringpropd  20176  imadrhmcl  20556  islmhm2  20793  lmhmpropd  20828  lbsextlem4  20919  prmirredlem  21243  psgndiflemA  21373  lsmcss  21464  uvcf1  21566  frlmsslsp  21570  frlmup1  21572  assapropd  21645  psrval  21687  evlslem1  21864  mamucl  22121  mamuass  22122  mamudi  22123  mamudir  22124  mamuvs1  22125  mamuvs2  22126  mamulid  22163  mamurid  22164  dmatsubcl  22220  dmatmulcl  22222  scmatscm  22235  marrepval  22284  marepveval  22290  mdetunilem7  22340  gsummatr01lem4  22380  cpmatmcllem  22440  mat2pmatf1  22451  mat2pmatlin  22457  decpmatmul  22494  pm2mpmhmlem2  22541  chpidmat  22569  pptbas  22731  toponmre  22817  restbas  22882  iscncl  22993  cnrest2  23010  cnpdis  23017  lmcnp  23028  dishaus  23106  cmpcovf  23115  tgcmp  23125  dfconn2  23143  clsconn  23154  2ndcctbss  23179  dis2ndc  23184  1stccnp  23186  islly2  23208  cldllycmp  23219  locfincmp  23250  comppfsc  23256  kgentopon  23262  txcls  23328  ptpjopn  23336  dfac14  23342  xkoccn  23343  txcnp  23344  txcmpb  23368  txlm  23372  xkopt  23379  xkoco1cn  23381  xkoco2cn  23382  qtopcn  23438  qtoprest  23441  regr1lem2  23464  xkocnv  23538  qtophmeo  23541  fmfnfmlem4  23681  hausflim  23705  hauspwpwf1  23711  fclscmp  23754  alexsublem  23768  alexsubALTlem2  23772  alexsubALTlem3  23773  ptcmplem3  23778  ptcmplem4  23779  ptcmplem5  23780  cnextfun  23788  tmdgsum2  23820  symgtgp  23830  tsmsval2  23854  tsmsgsum  23863  utoptop  23959  ismet2  24059  blin  24147  metss2lem  24240  methaus  24249  met1stc  24250  met2ndci  24251  prdsxmslem2  24258  metcnp3  24269  metcnpi3  24275  metustto  24282  metustfbas  24286  nlmvscn  24424  nrginvrcn  24429  xrsxmet  24545  reconnlem1  24562  reconn  24564  xrge0tsms  24570  xmetdcn2  24573  metdscn  24592  addcnlem  24600  fsumcn  24608  cnheiborlem  24700  cnheibor  24701  bndth  24704  lebnum  24710  nmoleub2lem2  24863  ipcn  24994  iscmet3  25041  caubl  25056  rrxdstprj1  25157  minveclem3b  25176  minveclem7  25183  pjthlem2  25186  pmltpc  25199  volfiniun  25296  ioombl1  25311  dyadss  25343  dyaddisjlem  25344  dyadmax  25347  dyadmbllem  25348  opnmbllem  25350  itg1addlem2  25446  itg10a  25460  mbfi1fseqlem6  25470  itg2seq  25492  itg2monolem1  25500  itg2gt0  25510  itgfsum  25576  limcfval  25621  ellimc2  25626  ellimc3  25628  limcres  25635  limciun  25643  dvres  25660  dveflem  25731  rolle  25742  dvlip2  25747  c1liplem1  25748  dvgt0lem1  25754  dvgt0  25756  dvlt0  25757  dvne0  25763  dvfsumrlimge0  25782  ftc1lem6  25793  itgsubst  25801  mdegmullem  25831  ply1domn  25876  ply1divex  25889  fta1g  25920  fta1b  25922  plyf  25947  dgrlem  25978  coeid  25987  plydivalg  26048  aannenlem1  26077  aalioulem3  26083  aalioulem6  26086  abelthlem8  26187  efif1olem4  26290  chordthm  26578  xrlimcnp  26709  jensen  26729  lgamcvglem  26780  lgamcvg2  26795  sqf11  26879  fsumvma2  26953  perfectlem2  26969  lgsdilem  27063  lgsquad2lem2  27124  lgsquad3  27126  2sqlem5  27161  2sqlem9  27166  2sqb  27171  rpvmasumlem  27226  dchrisum0flb  27249  dchrisum0  27259  pntpbnd  27327  pntibndlem3  27331  pntleml  27350  nolt02o  27434  nosupbday  27444  nosupbnd2  27455  noinfbday  27459  noinfbnd2  27470  noetasuplem4  27475  noetainflem4  27479  noetalem1  27480  conway  27537  slerec  27557  sltlpss  27638  addsprop  27698  tgjustc1  27993  tgjustc2  27994  legov  28103  legtrid  28109  tglinethru  28154  tglnpt2  28159  tglineintmo  28160  mirreu3  28172  perpcom  28231  colperpexlem3  28250  mideu  28256  opphllem1  28265  hlpasch  28274  lnopp2hpgb  28281  trgcopy  28322  brcgr  28425  brbtwn2  28430  colinearalg  28435  axsegcon  28452  axeuclidlem  28487  axcontlem9  28497  ecgrtg  28508  elntg  28509  eengtrkg  28511  upgr1eopALT  28644  usgredg4  28741  subuhgr  28810  subumgr  28812  usgr2wspthon  29486  clwlkclwwlkf1  29530  eupth2lems  29758  n4cyclfrgr  29811  vacn  30214  blocni  30325  ubthlem3  30392  minvecolem7  30403  chocunii  30821  pjhthmo  30822  pjhthlem2  30912  kbass5  31640  mdsymlem5  31927  foresf1o  32009  fcobij  32214  xrofsup  32247  mgcoval  32423  mgcf1o  32440  xrge0tsmsd  32479  symgcntz  32516  archirngz  32605  archiabllem2a  32610  isarchiofld  32705  prmidl2  32833  smatrcl  33074  reff  33117  ordtconnlem1  33202  qqhval2  33260  volmeas  33527  fiunelcarsg  33613  ballotlemfc0  33789  ballotlemfcc  33790  signstfvneq0  33881  derangenlem  34460  erdsze2lem1  34492  pconnconn  34520  connpconn  34524  cvxsconn  34532  cvmliftmolem2  34571  cvmliftmo  34573  cvmlift2lem10  34601  cvmlift2lem12  34603  cvmlift3lem7  34614  mrsubff1  34803  msubff1  34845  ifscgr  35320  cgrxfr  35331  btwnconn1lem13  35375  btwnconn1lem14  35376  outsideofeq  35406  ellines  35428  finminlem  35506  fnejoin2  35557  unbdqndv2  35690  irrdiff  36510  poimirlem13  36804  poimirlem14  36805  poimirlem32  36823  opnmbllem0  36827  mblfinlem3  36830  itg2addnclem  36842  itg2addnc  36845  ftc1cnnc  36863  upixp  36900  filbcmb  36911  sstotbnd2  36945  isbnd3  36955  prdsbnd2  36966  cntotbnd  36967  ismtyima  36974  bfp  36995  rrncmslem  37003  unichnidl  37202  lshpcmp  38161  islshpat  38190  lfl0f  38242  ishlat3N  38527  3dim1  38641  islvol5  38753  lvoli2  38755  lncvrelatN  38955  pclfinclN  39124  pexmidlem8N  39151  idltrn  39324  cdleme42keg  39660  cdleme42mgN  39662  cdlemf2  39736  cdlemg2cex  39765  trlcoat  39897  dihopelvalcpre  40422  dih1dimatlem  40503  dihjatcclem4  40595  lcfl7N  40675  lcfrlem9  40724  mapdh9a  40963  hdmapglem7  41103  aks4d1p8  41258  sticksstones11  41278  imacrhmcl  41393  fsuppind  41464  fsuppssind  41467  mhpind  41468  renegeulemv  41543  sn-subeu  41601  remulinvcom  41607  itrere  41641  retire  41642  prjspertr  41649  prjspreln0  41653  flt4lem7  41703  nna4b4nsq  41704  nacsfix  41752  mzpsubst  41788  mzpcompact2lem  41791  eldioph2lem2  41801  eldioph2  41802  eldioph2b  41803  diophin  41812  diophun  41813  irrapxlem3  41864  irrapxlem5  41866  pell1234qrreccl  41894  pell1234qrmulcl  41895  pell14qrdich  41909  pell1qrge1  41910  pell1qrgaplem  41913  monotuz  41982  acongtr  42019  acongrep  42021  jm2.23  42037  jm2.26a  42041  jm2.26lem3  42042  jm2.26  42043  jm2.27  42049  wepwsolem  42086  fnwe2lem2  42095  kelac1  42107  kercvrlsm  42127  hbtlem5  42172  hbt  42174  mpaaeu  42194  cantnfresb  42376  onmcl  42383  tfsconcatun  42389  tfsconcatfn  42390  tfsconcatfv1  42391  tfsconcatfv2  42392  naddcnff  42414  rfovcnvf1od  43057  mnurndlem1  43342  cncmpmax  44018  rfcnnnub  44022  disjxp1  44057  iccintsng  44534  fprodcn  44614  lptioo2  44645  lptioo1  44646  limclner  44665  stoweidlem31  45045  stoweidlem34  45048  stoweidlem35  45049  stoweidlem49  45063  stoweidlem59  45073  stoweidlem62  45076  fourierdlem60  45180  fourierdlem61  45181  fourierdlem87  45207  iundjiun  45474  ismeannd  45481  hoidmvle  45614  smfsuplem2  45826  2reu8i  46119  prproropf1olem2  46470  paireqne  46477  perfectALTVlem2  46688  mogoldbb  46751  bgoldbtbndlem2  46772  bgoldbtbndlem3  46773  isomgrtrlem  46804  mndpsuppss  47135  scmsuppss  47136  lindslinindsimp2lem5  47230  elfzolborelfzop1  47287  elbigolo1  47330  itschlc0xyqsol1  47539  itschlc0xyqsol  47540  iccdisj  47618  toslat  47694  functhinclem4  47751