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  5071  frpomin  6293  fsnex  7227  f1prex  7228  isotr  7280  weniso  7298  riota5f  7341  frxp2  8083  frxp3  8090  xpord3pred  8091  poseq  8097  fprlem2  8240  tfrlem9a  8314  oaass  8485  oeeui  8527  oaabs2  8574  coflton  8596  cofon1  8597  naddssim  8610  resixpfo  8873  omxpenlem  9005  pw2f1olem  9008  fopwdom  9012  fofinf1o  9231  marypha1lem  9335  ordiso2  9419  oismo  9444  ixpiunwdom  9494  cantnf  9603  ttrclss  9630  fseqenlem1  9935  iunfictbso  10025  dfac12lem2  10056  dfac12lem3  10057  infunsdom1  10123  infpssrlem5  10218  fin23lem24  10233  isf32lem2  10265  isf32lem4  10267  isf34lem4  10288  fin1a2lem12  10322  fin1a2lem13  10323  ttukeylem6  10425  fpwwe2lem11  10553  fpwwe2lem12  10554  fpwwe2  10555  winalim2  10608  wunex2  10650  tskord  10692  prlem934  10945  mulcmpblnr  10983  dedekind  11298  addrid  11315  cnegex  11316  negeu  11372  add20  11651  divdivdiv  11845  ltmul12a  12000  lemul12a  12002  lediv12a  12038  supaddc  12112  supmul1  12114  cru  12140  uzwo3  12882  xleadd1a  13194  xmullem  13205  xmulgt0  13224  xlemul1a  13229  ixxun  13303  ixxss12  13307  ioodisj  13424  fz0fzelfz0  13577  mulexpz  14053  rpexpmord  14119  leexp1a  14126  expmulnbnd  14186  hashf1  14408  fi1uzind  14458  brfi1indALT  14461  swrdccat  14686  reuccatpfxs1  14698  abs3lem  15290  rexanre  15298  cau3lem  15306  limsupgre  15432  limsupbnd2  15434  o1lo1  15488  rlimclim1  15496  rlimclim  15497  rlimcn1  15539  rlimcn3  15541  o1of2  15564  o1rlimmul  15570  lo1add  15578  lo1mul  15579  isercolllem1  15616  climcau  15622  caucvgrlem  15624  caucvgb  15631  summolem2  15667  summo  15668  modfsummod  15746  o1fsum  15765  prodmolem2  15889  addmodlteqALT  16283  rpdvds  16618  isprm5  16666  isprm6  16673  pclem  16798  pcqmul  16813  pcexp  16819  pcneg  16834  pcprmpw2  16842  pcadd  16849  pcmpt  16852  4sqlem13  16917  vdwlem2  16942  vdwlem7  16947  vdwlem12  16952  ramval  16968  ramub2  16974  ramz2  16984  ramcl  16989  cshwshashlem2  17056  imasval  17464  imasdsval  17468  mreexexd  17603  acsfn  17614  issubc3  17805  idfucl  17837  funcres2c  17859  isnat  17906  fucpropd  17936  xpcval  18132  xpcco  18138  prfval  18154  evlf2  18173  evlfcl  18177  curf12  18182  curf1cl  18183  curf2  18184  curfcl  18187  curf2ndf  18202  hof2val  18211  hofcl  18214  hofpropd  18222  yonedalem4a  18230  yonedainv  18236  drsdirfi  18260  pospo  18298  poslubmo  18364  posglbmo  18365  isipodrs  18492  acsinfd  18511  chnccat  18581  chnpof1  18585  gsumvalx  18633  gsumpropd2lem  18636  mgmhmeql  18673  sgrppropd  18688  ismndd  18713  mndpropd  18716  mndpsuppss  18722  mhmeql  18783  mndind  18785  frmdup3lem  18823  mhmmnd  19029  issubg4  19110  ssnmz  19130  conjnmzb  19217  f1otrspeq  19411  psgneu  19470  pgpfi  19569  sylow2blem3  19586  slwhash  19588  fislw  19589  sylow3lem2  19592  lsmdisj2  19646  pj1eu  19660  efgredlem  19711  frgpuplem  19736  gexex  19817  frgpnabl  19839  dprdfadd  19986  dpjidcl  20024  pgpfac1lem3  20043  pgpfaclem3  20049  ablfac2  20055  ablsimpgcygd  20072  ablsimpgfind  20076  ablsimpgprmd  20081  rngpropd  20144  ringpropd  20258  imadrhmcl  20763  islmhm2  21022  lmhmpropd  21057  lbsextlem4  21148  prmirredlem  21441  psgndiflemA  21570  lsmcss  21661  uvcf1  21761  frlmsslsp  21765  frlmup1  21767  assapropd  21840  psrval  21884  evlslem1  22049  mamucl  22354  mamuass  22355  mamudi  22356  mamudir  22357  mamuvs1  22358  mamuvs2  22359  mamulid  22394  mamurid  22395  dmatsubcl  22451  dmatmulcl  22453  scmatscm  22466  marrepval  22515  marepveval  22521  mdetunilem7  22571  gsummatr01lem4  22611  cpmatmcllem  22671  mat2pmatf1  22682  mat2pmatlin  22688  decpmatmul  22725  pm2mpmhmlem2  22772  chpidmat  22800  pptbas  22961  toponmre  23046  restbas  23111  iscncl  23222  cnrest2  23239  cnpdis  23246  lmcnp  23257  dishaus  23335  cmpcovf  23344  tgcmp  23354  dfconn2  23372  clsconn  23383  2ndcctbss  23408  dis2ndc  23413  1stccnp  23415  islly2  23437  cldllycmp  23448  locfincmp  23479  comppfsc  23485  kgentopon  23491  txcls  23557  ptpjopn  23565  dfac14  23571  xkoccn  23572  txcnp  23573  txcmpb  23597  txlm  23601  xkopt  23608  xkoco1cn  23610  xkoco2cn  23611  qtopcn  23667  qtoprest  23670  regr1lem2  23693  xkocnv  23767  qtophmeo  23770  fmfnfmlem4  23910  hausflim  23934  hauspwpwf1  23940  fclscmp  23983  alexsublem  23997  alexsubALTlem2  24001  alexsubALTlem3  24002  ptcmplem3  24007  ptcmplem4  24008  ptcmplem5  24009  cnextfun  24017  tmdgsum2  24049  symgtgp  24059  tsmsval2  24083  tsmsgsum  24092  utoptop  24187  ismet2  24286  blin  24374  metss2lem  24464  methaus  24473  met1stc  24474  met2ndci  24475  prdsxmslem2  24482  metcnp3  24493  metcnpi3  24499  metustto  24506  metustfbas  24510  nlmvscn  24640  nrginvrcn  24645  xrsxmet  24763  reconnlem1  24780  reconn  24782  xrge0tsms  24788  xmetdcn2  24791  metdscn  24810  addcnlem  24818  fsumcn  24825  cnheiborlem  24909  cnheibor  24910  bndth  24913  lebnum  24919  nmoleub2lem2  25071  ipcn  25201  iscmet3  25248  caubl  25263  rrxdstprj1  25364  minveclem3b  25383  minveclem7  25390  pjthlem2  25393  pmltpc  25405  volfiniun  25502  ioombl1  25517  dyadss  25549  dyaddisjlem  25550  dyadmax  25553  dyadmbllem  25554  opnmbllem  25556  itg1addlem2  25652  itg10a  25665  mbfi1fseqlem6  25675  itg2seq  25697  itg2monolem1  25705  itg2gt0  25715  itgfsum  25782  limcfval  25827  ellimc2  25832  ellimc3  25834  limcres  25841  limciun  25849  dvres  25866  dveflem  25934  rolle  25945  dvlip2  25950  c1liplem1  25951  dvgt0lem1  25957  dvgt0  25959  dvlt0  25960  dvne0  25966  dvfsumrlimge0  25985  ftc1lem6  25996  itgsubst  26004  mdegmullem  26031  ply1domn  26077  ply1divex  26090  fta1g  26123  fta1b  26125  plyf  26151  dgrlem  26182  coeid  26191  plydivalg  26253  aannenlem1  26282  aalioulem3  26288  aalioulem6  26291  abelthlem8  26392  efif1olem4  26497  chordthm  26789  xrlimcnp  26920  jensen  26940  lgamcvglem  26991  lgamcvg2  27006  sqf11  27090  fsumvma2  27165  perfectlem2  27181  lgsdilem  27275  lgsquad2lem2  27336  lgsquad3  27338  2sqlem5  27373  2sqlem9  27378  2sqb  27383  rpvmasumlem  27438  dchrisum0flb  27461  dchrisum0  27471  pntpbnd  27539  pntibndlem3  27543  pntleml  27562  nolt02o  27647  nosupbday  27657  nosupbnd2  27668  noinfbday  27672  noinfbnd2  27683  noetasuplem4  27688  noetainflem4  27692  noetalem1  27693  conway  27759  lesrec  27779  ltslpss  27888  addsprop  27956  bdayons  28256  n0fincut  28335  eucliddivs  28356  remulscllem2  28481  tgjustc1  28531  tgjustc2  28532  legov  28641  legtrid  28647  tglinethru  28692  tglnpt2  28697  tglineintmo  28698  mirreu3  28710  perpcom  28769  colperpexlem3  28788  mideu  28794  opphllem1  28803  hlpasch  28812  lnopp2hpgb  28819  trgcopy  28860  brcgr  28957  brbtwn2  28962  colinearalg  28967  axsegcon  28984  axeuclidlem  29019  axcontlem9  29029  ecgrtg  29040  elntg  29041  eengtrkg  29043  upgr1eopALT  29174  usgredg4  29274  subuhgr  29343  subumgr  29345  usgr2wspthon  30024  clwlkclwwlkf1  30068  eupth2lems  30296  n4cyclfrgr  30349  vacn  30753  blocni  30864  ubthlem3  30931  minvecolem7  30942  chocunii  31360  pjhthmo  31361  pjhthlem2  31451  kbass5  32179  mdsymlem5  32466  foresf1o  32562  fcobij  32781  xrofsup  32828  mgcoval  33034  mgcf1o  33051  xrge0tsmsd  33122  symgcntz  33134  archirngz  33238  archiabllem2a  33243  isarchiofld  33248  prmidl2  33489  mplvrpmmhm  33678  constrelextdg2  33879  smatrcl  33928  reff  33971  ordtconnlem1  34056  qqhval2  34114  volmeas  34363  fiunelcarsg  34448  ballotlemfc0  34625  ballotlemfcc  34626  signstfvneq0  34704  derangenlem  35341  erdsze2lem1  35373  pconnconn  35401  connpconn  35405  cvxsconn  35413  cvmliftmolem2  35452  cvmliftmo  35454  cvmlift2lem10  35482  cvmlift2lem12  35484  cvmlift3lem7  35495  mrsubff1  35684  msubff1  35726  r1peuqusdeg1  35813  ifscgr  36214  cgrxfr  36225  btwnconn1lem13  36269  btwnconn1lem14  36270  outsideofeq  36300  ellines  36322  finminlem  36488  fnejoin2  36539  weiunso  36636  unbdqndv2  36759  irrdiff  37628  qdiff  37629  poimirlem13  37942  poimirlem14  37943  poimirlem32  37961  opnmbllem0  37965  mblfinlem3  37968  itg2addnclem  37980  itg2addnc  37983  ftc1cnnc  38001  upixp  38038  filbcmb  38049  sstotbnd2  38083  isbnd3  38093  prdsbnd2  38104  cntotbnd  38105  ismtyima  38112  bfp  38133  rrncmslem  38141  unichnidl  38340  lshpcmp  39422  islshpat  39451  lfl0f  39503  ishlat3N  39788  3dim1  39901  islvol5  40013  lvoli2  40015  lncvrelatN  40215  pclfinclN  40384  pexmidlem8N  40411  idltrn  40584  cdleme42keg  40920  cdleme42mgN  40922  cdlemf2  40996  cdlemg2cex  41025  trlcoat  41157  dihopelvalcpre  41682  dih1dimatlem  41763  dihjatcclem4  41855  lcfl7N  41935  lcfrlem9  41984  mapdh9a  42223  hdmapglem7  42363  aks4d1p8  42514  isprimroot  42520  evl1gprodd  42544  sticksstones11  42583  grpods  42621  aks5lem8  42628  renegeulemv  42788  sn-subeu  42847  remulinvcom  42853  imacrhmcl  42947  fidomncyc  42968  fsuppind  43011  fsuppssind  43014  mhpind  43015  prjspertr  43026  prjspreln0  43030  flt4lem7  43080  nna4b4nsq  43081  nacsfix  43132  mzpsubst  43168  mzpcompact2lem  43171  eldioph2lem2  43181  eldioph2  43182  eldioph2b  43183  diophin  43192  diophun  43193  irrapxlem3  43240  irrapxlem5  43242  pell1234qrreccl  43270  pell1234qrmulcl  43271  pell14qrdich  43285  pell1qrge1  43286  pell1qrgaplem  43289  monotuz  43357  acongtr  43394  acongrep  43396  jm2.23  43412  jm2.26a  43416  jm2.26lem3  43417  jm2.26  43418  jm2.27  43424  wepwsolem  43458  fnwe2lem2  43467  kelac1  43479  kercvrlsm  43499  hbtlem5  43544  hbt  43546  mpaaeu  43566  cantnfresb  43740  onmcl  43747  tfsconcatun  43753  tfsconcatfn  43754  tfsconcatfv1  43755  tfsconcatfv2  43756  naddcnff  43778  rfovcnvf1od  44419  mnurndlem1  44696  cncmpmax  45451  rfcnnnub  45455  disjxp1  45488  iccintsng  45941  fprodcn  46018  lptioo2  46049  lptioo1  46050  limclner  46067  stoweidlem31  46447  stoweidlem34  46450  stoweidlem35  46451  stoweidlem49  46465  stoweidlem59  46475  stoweidlem62  46478  fourierdlem60  46582  fourierdlem61  46583  fourierdlem87  46609  iundjiun  46876  ismeannd  46883  hoidmvle  47016  smfsuplem2  47228  2reu8i  47549  prproropf1olem2  47952  paireqne  47959  nprmmul2  47976  perfectALTVlem2  48186  mogoldbb  48249  bgoldbtbndlem2  48270  bgoldbtbndlem3  48271  grimedg  48399  grlimprclnbgrvtx  48463  scmsuppss  48835  lindslinindsimp2lem5  48926  elfzolborelfzop1  48983  elbigolo1  49021  itschlc0xyqsol1  49230  itschlc0xyqsol  49231  iccdisj  49361  toslat  49445  iinfssclem3  49519  iinfssc  49520  iinfsubc  49521  imasubc3  49619  upciclem4  49632  uppropd  49644  natoppf  49692  tposcurf1  49762  fuco22  49802  fuco22natlem  49808  functhinclem4  49910  arweuthinc  49992