Theorem simplrr 787

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  disjxiun  5098  frpomin  6327  fsnex  7267  f1prex  7268  isotr  7320  weniso  7338  riota5f  7381  frxp2  8124  frxp3  8131  xpord3pred  8132  poseq  8138  fprlem2  8282  tfrlem9a  8357  oaass  8530  oeeui  8572  oaabs2  8619  coflton  8641  cofon1  8642  naddssim  8656  resixpfo  8918  omxpenlem  9050  pw2f1olem  9053  fopwdom  9057  fofinf1o  9273  marypha1lem  9377  ordiso2  9461  oismo  9486  ixpiunwdom  9536  cantnf  9646  ttrclss  9673  fseqenlem1  9992  iunfictbso  10082  dfac12lem2  10112  dfac12lem3  10113  infunsdom1  10179  infpssrlem5  10275  fin23lem24  10290  isf32lem2  10322  isf32lem4  10324  isf34lem4  10345  fin1a2lem12  10379  fin1a2lem13  10380  ttukeylem6  10482  fpwwe2lem11  10610  fpwwe2lem12  10611  fpwwe2  10612  winalim2  10665  wunex2  10707  tskord  10749  prlem934  11002  mulcmpblnr  11040  dedekind  11357  addrid  11374  cnegex  11375  negeu  11431  add20  11710  divdivdiv  11903  ltmul12a  12058  lemul12a  12060  lediv12a  12095  supaddc  12169  supmul1  12171  cru  12197  uzwo3  12954  xleadd1a  13266  xmullem  13277  xmulgt0  13296  xlemul1a  13301  ixxun  13375  ixxss12  13379  ioodisj  13496  fz0fzelfz0  13649  mulexpz  14125  rpexpmord  14191  leexp1a  14198  expmulnbnd  14258  hashf1  14480  fi1uzind  14530  brfi1indALT  14533  swrdccat  14758  reuccatpfxs1  14770  abs3lem  15376  rexanre  15384  cau3lem  15392  limsupgre  15518  limsupbnd2  15520  o1lo1  15574  rlimclim1  15582  rlimclim  15583  rlimcn1  15625  rlimcn3  15627  o1of2  15650  o1rlimmul  15656  lo1add  15664  lo1mul  15665  isercolllem1  15702  climcau  15708  caucvgrlem  15710  caucvgb  15717  summolem2  15753  summo  15754  modfsummod  15832  o1fsum  15851  prodmolem2  15975  addmodlteqALT  16369  rpdvds  16704  isprm5  16752  isprm6  16759  pclem  16884  pcqmul  16899  pcexp  16905  pcneg  16920  pcprmpw2  16928  pcadd  16935  pcmpt  16938  4sqlem13  17003  vdwlem2  17028  vdwlem7  17033  vdwlem12  17038  ramval  17054  ramub2  17060  ramz2  17070  ramcl  17075  cshwshashlem2  17142  imasval  17551  imasdsval  17555  mreexexd  17690  acsfn  17701  issubc3  17892  idfucl  17924  funcres2c  17946  isnat  17993  fucpropd  18023  xpcval  18219  xpcco  18225  prfval  18241  evlf2  18260  evlfcl  18264  curf12  18269  curf1cl  18270  curf2  18271  curfcl  18274  curf2ndf  18289  hof2val  18298  hofcl  18301  hofpropd  18309  yonedalem4a  18317  yonedainv  18323  drsdirfi  18347  pospo  18385  poslubmo  18451  posglbmo  18452  isipodrs  18579  acsinfd  18598  chnccat  18668  chnpof1  18672  gsumvalx  18720  gsumpropd2lem  18723  mgmhmeql  18760  sgrppropd  18775  ismndd  18800  mndpropd  18803  mndpsuppss  18809  mhmeql  18870  mndind  18872  frmdup3lem  18910  mhmmnd  19116  issubg4  19197  ssnmz  19217  conjnmzb  19303  f1otrspeq  19497  psgneu  19556  pgpfi  19655  sylow2blem3  19672  slwhash  19674  fislw  19675  sylow3lem2  19678  lsmdisj2  19732  pj1eu  19746  efgredlem  19797  frgpuplem  19822  gexex  19903  frgpnabl  19925  dprdfadd  20072  dpjidcl  20110  pgpfac1lem3  20129  pgpfaclem3  20135  ablfac2  20141  ablsimpgcygd  20158  ablsimpgfind  20162  ablsimpgprmd  20167  rngpropd  20230  ringpropd  20348  imadrhmcl  20853  islmhm2  21112  lmhmpropd  21147  lbsextlem4  21238  prmirredlem  21531  psgndiflemA  21660  lsmcss  21751  uvcf1  21851  frlmsslsp  21855  frlmup1  21857  assapropd  21930  psrval  21974  evlslem1  22142  mamucl  22468  mamuass  22469  mamudi  22470  mamudir  22471  mamuvs1  22472  mamuvs2  22473  mamulid  22508  mamurid  22509  dmatsubcl  22565  dmatmulcl  22567  scmatscm  22580  marrepval  22629  marepveval  22635  mdetunilem7  22685  gsummatr01lem4  22725  cpmatmcllem  22785  mat2pmatf1  22796  mat2pmatlin  22802  decpmatmul  22839  pm2mpmhmlem2  22886  chpidmat  22914  pptbas  23075  toponmre  23160  restbas  23225  iscncl  23336  cnrest2  23353  cnpdis  23360  lmcnp  23371  dishaus  23449  cmpcovf  23458  tgcmp  23468  dfconn2  23486  clsconn  23497  2ndcctbss  23522  dis2ndc  23527  1stccnp  23529  islly2  23551  cldllycmp  23562  locfincmp  23593  comppfsc  23599  kgentopon  23605  txcls  23671  ptpjopn  23679  dfac14  23685  xkoccn  23686  txcnp  23687  txcmpb  23711  txlm  23715  xkopt  23722  xkoco1cn  23724  xkoco2cn  23725  qtopcn  23781  qtoprest  23784  regr1lem2  23807  xkocnv  23881  qtophmeo  23884  fmfnfmlem4  24024  hausflim  24048  hauspwpwf1  24054  fclscmp  24097  alexsublem  24111  alexsubALTlem2  24115  alexsubALTlem3  24116  ptcmplem3  24121  ptcmplem4  24122  ptcmplem5  24123  cnextfun  24131  tmdgsum2  24163  symgtgp  24173  tsmsval2  24197  tsmsgsum  24206  utoptop  24301  ismet2  24400  blin  24488  metss2lem  24578  methaus  24587  met1stc  24588  met2ndci  24589  prdsxmslem2  24596  metcnp3  24607  metcnpi3  24613  metustto  24620  metustfbas  24624  nlmvscn  24754  nrginvrcn  24759  xrsxmet  24877  reconnlem1  24894  reconn  24896  xrge0tsms  24902  xmetdcn2  24905  metdscn  24924  addcnlem  24932  fsumcn  24939  cnheiborlem  25023  cnheibor  25024  bndth  25027  lebnum  25033  nmoleub2lem2  25185  ipcn  25315  iscmet3  25362  caubl  25377  rrxdstprj1  25478  minveclem3b  25497  minveclem7  25504  pjthlem2  25507  pmltpc  25519  volfiniun  25616  ioombl1  25631  dyadss  25663  dyaddisjlem  25664  dyadmax  25667  dyadmbllem  25668  opnmbllem  25670  itg1addlem2  25766  itg10a  25779  mbfi1fseqlem6  25789  itg2seq  25811  itg2monolem1  25819  itg2gt0  25829  itgfsum  25896  limcfval  25941  ellimc2  25946  ellimc3  25948  limcres  25955  limciun  25963  dvres  25980  dveflem  26048  rolle  26059  dvlip2  26064  c1liplem1  26065  dvgt0lem1  26071  dvgt0  26073  dvlt0  26074  dvne0  26080  dvfsumrlimge0  26099  ftc1lem6  26110  itgsubst  26118  mdegmullem  26145  ply1domn  26191  ply1divex  26204  fta1g  26237  fta1b  26239  plyf  26265  dgrlem  26296  coeid  26305  plydivalg  26370  aannenlem1  26399  aalioulem3  26405  aalioulem6  26408  abelthlem8  26509  efif1olem4  26617  chordthm  26909  xrlimcnp  27040  jensen  27060  lgamcvglem  27111  lgamcvg2  27126  sqf11  27210  fsumvma2  27285  perfectlem2  27301  lgsdilem  27395  lgsquad2lem2  27456  lgsquad3  27458  2sqlem5  27493  2sqlem9  27498  2sqb  27503  rpvmasumlem  27558  dchrisum0flb  27581  dchrisum0  27591  pntpbnd  27659  pntibndlem3  27663  pntleml  27682  nolt02o  27766  nosupbday  27776  nosupbnd2  27787  noinfbday  27791  noinfbnd2  27802  noetasuplem4  27807  noetainflem4  27811  noetalem1  27812  conway  27879  lesrec  27899  ltslpss  28008  addsprop  28076  bdayons  28376  n0fincut  28455  eucliddivs  28476  remulscllem2  28601  tgjustc1  28651  tgjustc2  28652  legov  28761  legtrid  28767  tglinethru  28812  tglineintmo  28818  tglnpt2  28829  mirreu3  28834  perpcom  28893  colperpexlem3  28912  mideu  28918  opphllem1  28927  hlpasch  28936  lnopp2hpgb  28943  trgcopy  28984  brcgr  29108  brbtwn2  29113  colinearalg  29118  axsegcon  29135  axeuclidlem  29170  axcontlem9  29180  ecgrtg  29191  elntg  29192  eengtrkg  29194  upgr1eopALT  29325  usgredg4  29425  subuhgr  29494  subumgr  29496  usgr2wspthon  30175  clwlkclwwlkf1  30219  eupth2lems  30447  n4cyclfrgr  30500  vacn  30904  blocni  31015  ubthlem3  31082  minvecolem7  31093  chocunii  31511  pjhthmo  31512  pjhthlem2  31602  kbass5  32330  mdsymlem5  32617  foresf1o  32709  fcobij  32928  xrofsup  32975  mgcoval  33170  mgcf1o  33187  xrge0tsmsd  33259  symgcntz  33271  archirngz  33375  archiabllem2a  33380  isarchiofld  33385  prmidl2  33630  mplvrpmmhm  33845  constrelextdg2  34046  smatrcl  34095  reff  34138  ordtconnlem1  34223  qqhval2  34281  volmeas  34530  fiunelcarsg  34615  ballotlemfc0  34792  ballotlemfcc  34793  signstfvneq0  34868  derangenlem  35526  erdsze2lem1  35558  pconnconn  35586  connpconn  35590  cvxsconn  35598  cvmliftmolem2  35637  cvmliftmo  35639  cvmlift2lem10  35667  cvmlift2lem12  35669  cvmlift3lem7  35680  mrsubff1  35869  msubff1  35911  r1peuqusdeg1  35998  ifscgr  36399  cgrxfr  36410  btwnconn1lem13  36454  btwnconn1lem14  36455  outsideofeq  36485  ellines  36507  finminlem  36683  fnejoin2  36734  weiunso  36831  unbdqndv2  36954  irrdiff  37823  qdiff  37824  poimirlem13  38137  poimirlem14  38138  poimirlem32  38156  opnmbllem0  38160  mblfinlem3  38163  itg2addnclem  38175  itg2addnc  38178  ftc1cnnc  38196  upixp  38233  filbcmb  38244  sstotbnd2  38278  isbnd3  38288  prdsbnd2  38299  cntotbnd  38300  ismtyima  38307  bfp  38328  rrncmslem  38336  unichnidl  38535  lshpcmp  39617  islshpat  39646  lfl0f  39698  ishlat3N  39983  3dim1  40096  islvol5  40208  lvoli2  40210  lncvrelatN  40410  pclfinclN  40579  pexmidlem8N  40606  idltrn  40779  cdleme42keg  41115  cdleme42mgN  41117  cdlemf2  41191  cdlemg2cex  41220  trlcoat  41352  dihopelvalcpre  41877  dih1dimatlem  41958  dihjatcclem4  42050  lcfl7N  42130  lcfrlem9  42179  mapdh9a  42418  hdmapglem7  42558  aks4d1p8  42709  isprimroot  42715  evl1gprodd  42739  sticksstones11  42778  grpods  42816  aks5lem8  42823  renegeulemv  42982  sn-subeu  43041  remulinvcom  43047  imacrhmcl  43141  fidomncyc  43158  fsuppind  43177  fsuppssind  43180  mhpind  43181  prjspertr  43192  prjspreln0  43196  flt4lem7  43246  nna4b4nsq  43247  nacsfix  43298  mzpsubst  43334  mzpcompact2lem  43337  eldioph2lem2  43347  eldioph2  43348  eldioph2b  43349  diophin  43358  diophun  43359  irrapxlem3  43406  irrapxlem5  43408  pell1234qrreccl  43436  pell1234qrmulcl  43437  pell14qrdich  43451  pell1qrge1  43452  pell1qrgaplem  43455  monotuz  43523  acongtr  43560  acongrep  43562  jm2.23  43578  jm2.26a  43582  jm2.26lem3  43583  jm2.26  43584  jm2.27  43590  wepwsolem  43624  fnwe2lem2  43633  kelac1  43645  kercvrlsm  43665  hbtlem5  43710  hbt  43712  mpaaeu  43732  cantnfresb  43906  onmcl  43913  tfsconcatun  43919  tfsconcatfn  43920  tfsconcatfv1  43921  tfsconcatfv2  43922  naddcnff  43944  rfovcnvf1od  44585  mnurndlem1  44848  cncmpmax  45603  rfcnnnub  45607  disjxp1  45640  iccintsng  46090  fprodcn  46167  lptioo2  46198  lptioo1  46199  limclner  46216  stoweidlem31  46596  stoweidlem34  46599  stoweidlem35  46600  stoweidlem49  46614  stoweidlem59  46624  stoweidlem62  46627  fourierdlem60  46731  fourierdlem61  46732  fourierdlem87  46758  iundjiun  47025  ismeannd  47032  hoidmvle  47165  smfsuplem2  47377  2reu8i  47698  prproropf1olem2  48101  paireqne  48108  nprmmul2  48125  perfectALTVlem2  48335  mogoldbb  48398  bgoldbtbndlem2  48419  bgoldbtbndlem3  48420  grimedg  48548  grlimprclnbgrvtx  48612  scmsuppss  48984  lindslinindsimp2lem5  49075  elfzolborelfzop1  49132  elbigolo1  49170  itschlc0xyqsol1  49379  itschlc0xyqsol  49380  iccdisj  49510  toslat  49594  iinfssclem3  49668  iinfssc  49669  iinfsubc  49670  imasubc3  49768  upciclem4  49781  uppropd  49793  natoppf  49841  tposcurf1  49911  fuco22  49951  fuco22natlem  49957  functhinclem4  50059  arweuthinc  50141