Theorem simplrr 778

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 484	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 728	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:  disjxiun  5083  frpomin  6305  fsnex  7238  f1prex  7239  isotr  7291  weniso  7309  riota5f  7352  frxp2  8094  frxp3  8101  xpord3pred  8102  poseq  8108  fprlem2  8251  tfrlem9a  8325  oaass  8496  oeeui  8538  oaabs2  8585  coflton  8607  cofon1  8608  naddssim  8621  resixpfo  8884  omxpenlem  9016  pw2f1olem  9019  fopwdom  9023  fofinf1o  9242  marypha1lem  9346  ordiso2  9430  oismo  9455  ixpiunwdom  9505  cantnf  9614  ttrclss  9641  fseqenlem1  9946  iunfictbso  10036  dfac12lem2  10067  dfac12lem3  10068  infunsdom1  10134  infpssrlem5  10229  fin23lem24  10244  isf32lem2  10276  isf32lem4  10278  isf34lem4  10299  fin1a2lem12  10333  fin1a2lem13  10334  ttukeylem6  10436  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  winalim2  10619  wunex2  10661  tskord  10703  prlem934  10956  mulcmpblnr  10994  dedekind  11309  addrid  11326  cnegex  11327  negeu  11383  add20  11662  divdivdiv  11856  ltmul12a  12011  lemul12a  12013  lediv12a  12049  supaddc  12123  supmul1  12125  cru  12151  uzwo3  12893  xleadd1a  13205  xmullem  13216  xmulgt0  13235  xlemul1a  13240  ixxun  13314  ixxss12  13318  ioodisj  13435  fz0fzelfz0  13588  mulexpz  14064  rpexpmord  14130  leexp1a  14137  expmulnbnd  14197  hashf1  14419  fi1uzind  14469  brfi1indALT  14472  swrdccat  14697  reuccatpfxs1  14709  abs3lem  15301  rexanre  15309  cau3lem  15317  limsupgre  15443  limsupbnd2  15445  o1lo1  15499  rlimclim1  15507  rlimclim  15508  rlimcn1  15550  rlimcn3  15552  o1of2  15575  o1rlimmul  15581  lo1add  15589  lo1mul  15590  isercolllem1  15627  climcau  15633  caucvgrlem  15635  caucvgb  15642  summolem2  15678  summo  15679  modfsummod  15757  o1fsum  15776  prodmolem2  15900  addmodlteqALT  16294  rpdvds  16629  isprm5  16677  isprm6  16684  pclem  16809  pcqmul  16824  pcexp  16830  pcneg  16845  pcprmpw2  16853  pcadd  16860  pcmpt  16863  4sqlem13  16928  vdwlem2  16953  vdwlem7  16958  vdwlem12  16963  ramval  16979  ramub2  16985  ramz2  16995  ramcl  17000  cshwshashlem2  17067  imasval  17475  imasdsval  17479  mreexexd  17614  acsfn  17625  issubc3  17816  idfucl  17848  funcres2c  17870  isnat  17917  fucpropd  17947  xpcval  18143  xpcco  18149  prfval  18165  evlf2  18184  evlfcl  18188  curf12  18193  curf1cl  18194  curf2  18195  curfcl  18198  curf2ndf  18213  hof2val  18222  hofcl  18225  hofpropd  18233  yonedalem4a  18241  yonedainv  18247  drsdirfi  18271  pospo  18309  poslubmo  18375  posglbmo  18376  isipodrs  18503  acsinfd  18522  chnccat  18592  chnpof1  18596  gsumvalx  18644  gsumpropd2lem  18647  mgmhmeql  18684  sgrppropd  18699  ismndd  18724  mndpropd  18727  mndpsuppss  18733  mhmeql  18794  mndind  18796  frmdup3lem  18834  mhmmnd  19040  issubg4  19121  ssnmz  19141  conjnmzb  19228  f1otrspeq  19422  psgneu  19481  pgpfi  19580  sylow2blem3  19597  slwhash  19599  fislw  19600  sylow3lem2  19603  lsmdisj2  19657  pj1eu  19671  efgredlem  19722  frgpuplem  19747  gexex  19828  frgpnabl  19850  dprdfadd  19997  dpjidcl  20035  pgpfac1lem3  20054  pgpfaclem3  20060  ablfac2  20066  ablsimpgcygd  20083  ablsimpgfind  20087  ablsimpgprmd  20092  rngpropd  20155  ringpropd  20269  imadrhmcl  20774  islmhm2  21033  lmhmpropd  21068  lbsextlem4  21159  prmirredlem  21452  psgndiflemA  21581  lsmcss  21672  uvcf1  21772  frlmsslsp  21776  frlmup1  21778  assapropd  21851  psrval  21895  evlslem1  22060  mamucl  22366  mamuass  22367  mamudi  22368  mamudir  22369  mamuvs1  22370  mamuvs2  22371  mamulid  22406  mamurid  22407  dmatsubcl  22463  dmatmulcl  22465  scmatscm  22478  marrepval  22527  marepveval  22533  mdetunilem7  22583  gsummatr01lem4  22623  cpmatmcllem  22683  mat2pmatf1  22694  mat2pmatlin  22700  decpmatmul  22737  pm2mpmhmlem2  22784  chpidmat  22812  pptbas  22973  toponmre  23058  restbas  23123  iscncl  23234  cnrest2  23251  cnpdis  23258  lmcnp  23269  dishaus  23347  cmpcovf  23356  tgcmp  23366  dfconn2  23384  clsconn  23395  2ndcctbss  23420  dis2ndc  23425  1stccnp  23427  islly2  23449  cldllycmp  23460  locfincmp  23491  comppfsc  23497  kgentopon  23503  txcls  23569  ptpjopn  23577  dfac14  23583  xkoccn  23584  txcnp  23585  txcmpb  23609  txlm  23613  xkopt  23620  xkoco1cn  23622  xkoco2cn  23623  qtopcn  23679  qtoprest  23682  regr1lem2  23705  xkocnv  23779  qtophmeo  23782  fmfnfmlem4  23922  hausflim  23946  hauspwpwf1  23952  fclscmp  23995  alexsublem  24009  alexsubALTlem2  24013  alexsubALTlem3  24014  ptcmplem3  24019  ptcmplem4  24020  ptcmplem5  24021  cnextfun  24029  tmdgsum2  24061  symgtgp  24071  tsmsval2  24095  tsmsgsum  24104  utoptop  24199  ismet2  24298  blin  24386  metss2lem  24476  methaus  24485  met1stc  24486  met2ndci  24487  prdsxmslem2  24494  metcnp3  24505  metcnpi3  24511  metustto  24518  metustfbas  24522  nlmvscn  24652  nrginvrcn  24657  xrsxmet  24775  reconnlem1  24792  reconn  24794  xrge0tsms  24800  xmetdcn2  24803  metdscn  24822  addcnlem  24830  fsumcn  24837  cnheiborlem  24921  cnheibor  24922  bndth  24925  lebnum  24931  nmoleub2lem2  25083  ipcn  25213  iscmet3  25260  caubl  25275  rrxdstprj1  25376  minveclem3b  25395  minveclem7  25402  pjthlem2  25405  pmltpc  25417  volfiniun  25514  ioombl1  25529  dyadss  25561  dyaddisjlem  25562  dyadmax  25565  dyadmbllem  25566  opnmbllem  25568  itg1addlem2  25664  itg10a  25677  mbfi1fseqlem6  25687  itg2seq  25709  itg2monolem1  25717  itg2gt0  25727  itgfsum  25794  limcfval  25839  ellimc2  25844  ellimc3  25846  limcres  25853  limciun  25861  dvres  25878  dveflem  25946  rolle  25957  dvlip2  25962  c1liplem1  25963  dvgt0lem1  25969  dvgt0  25971  dvlt0  25972  dvne0  25978  dvfsumrlimge0  25997  ftc1lem6  26008  itgsubst  26016  mdegmullem  26043  ply1domn  26089  ply1divex  26102  fta1g  26135  fta1b  26137  plyf  26163  dgrlem  26194  coeid  26203  plydivalg  26265  aannenlem1  26294  aalioulem3  26300  aalioulem6  26303  abelthlem8  26404  efif1olem4  26509  chordthm  26801  xrlimcnp  26932  jensen  26952  lgamcvglem  27003  lgamcvg2  27018  sqf11  27102  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  27659  nosupbday  27669  nosupbnd2  27680  noinfbday  27684  noinfbnd2  27695  noetasuplem4  27700  noetainflem4  27704  noetalem1  27705  conway  27771  lesrec  27791  ltslpss  27900  addsprop  27968  bdayons  28268  n0fincut  28347  eucliddivs  28368  remulscllem2  28493  tgjustc1  28543  tgjustc2  28544  legov  28653  legtrid  28659  tglinethru  28704  tglnpt2  28709  tglineintmo  28710  mirreu3  28722  perpcom  28781  colperpexlem3  28800  mideu  28806  opphllem1  28815  hlpasch  28824  lnopp2hpgb  28831  trgcopy  28872  brcgr  28969  brbtwn2  28974  colinearalg  28979  axsegcon  28996  axeuclidlem  29031  axcontlem9  29041  ecgrtg  29052  elntg  29053  eengtrkg  29055  upgr1eopALT  29186  usgredg4  29286  subuhgr  29355  subumgr  29357  usgr2wspthon  30036  clwlkclwwlkf1  30080  eupth2lems  30308  n4cyclfrgr  30361  vacn  30765  blocni  30876  ubthlem3  30943  minvecolem7  30954  chocunii  31372  pjhthmo  31373  pjhthlem2  31463  kbass5  32191  mdsymlem5  32478  foresf1o  32574  fcobij  32793  xrofsup  32840  mgcoval  33046  mgcf1o  33063  xrge0tsmsd  33134  symgcntz  33146  archirngz  33250  archiabllem2a  33255  isarchiofld  33260  prmidl2  33501  mplvrpmmhm  33690  constrelextdg2  33891  smatrcl  33940  reff  33983  ordtconnlem1  34068  qqhval2  34126  volmeas  34375  fiunelcarsg  34460  ballotlemfc0  34637  ballotlemfcc  34638  signstfvneq0  34716  derangenlem  35353  erdsze2lem1  35385  pconnconn  35413  connpconn  35417  cvxsconn  35425  cvmliftmolem2  35464  cvmliftmo  35466  cvmlift2lem10  35494  cvmlift2lem12  35496  cvmlift3lem7  35507  mrsubff1  35696  msubff1  35738  r1peuqusdeg1  35825  ifscgr  36226  cgrxfr  36237  btwnconn1lem13  36281  btwnconn1lem14  36282  outsideofeq  36312  ellines  36334  finminlem  36500  fnejoin2  36551  weiunso  36648  unbdqndv2  36771  irrdiff  37640  qdiff  37641  poimirlem13  37954  poimirlem14  37955  poimirlem32  37973  opnmbllem0  37977  mblfinlem3  37980  itg2addnclem  37992  itg2addnc  37995  ftc1cnnc  38013  upixp  38050  filbcmb  38061  sstotbnd2  38095  isbnd3  38105  prdsbnd2  38116  cntotbnd  38117  ismtyima  38124  bfp  38145  rrncmslem  38153  unichnidl  38352  lshpcmp  39434  islshpat  39463  lfl0f  39515  ishlat3N  39800  3dim1  39913  islvol5  40025  lvoli2  40027  lncvrelatN  40227  pclfinclN  40396  pexmidlem8N  40423  idltrn  40596  cdleme42keg  40932  cdleme42mgN  40934  cdlemf2  41008  cdlemg2cex  41037  trlcoat  41169  dihopelvalcpre  41694  dih1dimatlem  41775  dihjatcclem4  41867  lcfl7N  41947  lcfrlem9  41996  mapdh9a  42235  hdmapglem7  42375  aks4d1p8  42526  isprimroot  42532  evl1gprodd  42556  sticksstones11  42595  grpods  42633  aks5lem8  42640  renegeulemv  42800  sn-subeu  42859  remulinvcom  42865  imacrhmcl  42959  fidomncyc  42980  fsuppind  43023  fsuppssind  43026  mhpind  43027  prjspertr  43038  prjspreln0  43042  flt4lem7  43092  nna4b4nsq  43093  nacsfix  43144  mzpsubst  43180  mzpcompact2lem  43183  eldioph2lem2  43193  eldioph2  43194  eldioph2b  43195  diophin  43204  diophun  43205  irrapxlem3  43252  irrapxlem5  43254  pell1234qrreccl  43282  pell1234qrmulcl  43283  pell14qrdich  43297  pell1qrge1  43298  pell1qrgaplem  43301  monotuz  43369  acongtr  43406  acongrep  43408  jm2.23  43424  jm2.26a  43428  jm2.26lem3  43429  jm2.26  43430  jm2.27  43436  wepwsolem  43470  fnwe2lem2  43479  kelac1  43491  kercvrlsm  43511  hbtlem5  43556  hbt  43558  mpaaeu  43578  cantnfresb  43752  onmcl  43759  tfsconcatun  43765  tfsconcatfn  43766  tfsconcatfv1  43767  tfsconcatfv2  43768  naddcnff  43790  rfovcnvf1od  44431  mnurndlem1  44708  cncmpmax  45463  rfcnnnub  45467  disjxp1  45500  iccintsng  45953  fprodcn  46030  lptioo2  46061  lptioo1  46062  limclner  46079  stoweidlem31  46459  stoweidlem34  46462  stoweidlem35  46463  stoweidlem49  46477  stoweidlem59  46487  stoweidlem62  46490  fourierdlem60  46594  fourierdlem61  46595  fourierdlem87  46621  iundjiun  46888  ismeannd  46895  hoidmvle  47028  smfsuplem2  47240  2reu8i  47555  prproropf1olem2  47958  paireqne  47965  nprmmul2  47982  perfectALTVlem2  48192  mogoldbb  48255  bgoldbtbndlem2  48276  bgoldbtbndlem3  48277  grimedg  48405  grlimprclnbgrvtx  48469  scmsuppss  48841  lindslinindsimp2lem5  48932  elfzolborelfzop1  48989  elbigolo1  49027  itschlc0xyqsol1  49236  itschlc0xyqsol  49237  iccdisj  49367  toslat  49451  iinfssclem3  49525  iinfssc  49526  iinfsubc  49527  imasubc3  49625  upciclem4  49638  uppropd  49650  natoppf  49698  tposcurf1  49768  fuco22  49808  fuco22natlem  49814  functhinclem4  49916  arweuthinc  49998