Theorem simplrr 790

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  disjxiun  5103  frpomin  6361  fsnex  7314  f1prex  7315  isotr  7367  weniso  7387  riota5f  7428  fnwe2lem3  8174  frxp2  8188  frxp3  8195  xpord3pred  8196  poseq  8202  fprlem2  8347  tfrlem9a  8422  oaass  8597  oeeui  8639  oaabs2  8686  coflton  8708  cofon1  8709  naddssim  8723  resixpfo  8992  omxpenlem  9125  pw2f1olem  9128  fopwdom  9132  fofinf1o  9349  marypha1lem  9452  ordiso2  9536  oismo  9561  ixpiunwdom  9611  cantnf  9721  ttrclss  9748  fseqenlem1  10130  iunfictbso  10220  dfac12lem2  10250  dfac12lem3  10251  infunsdom1  10317  infpssrlem5  10412  fin23lem24  10427  isf32lem2  10459  isf32lem4  10461  isf34lem4  10482  fin1a2lem12  10516  fin1a2lem13  10517  ttukeylem6  10619  fpwwe2lem11  10753  fpwwe2lem12  10754  fpwwe2  10755  winalim2  10808  wunex2  10850  tskord  10892  prlem934  11145  mulcmpblnr  11183  dedekind  11500  addrid  11517  cnegex  11518  negeu  11574  add20  11855  divdivdiv  12045  ltmul12a  12200  lemul12a  12202  lediv12a  12237  supaddc  12311  supmul1  12313  cru  12339  uzwo3  13097  xleadd1a  13410  xmullem  13421  xmulgt0  13440  xlemul1a  13445  ixxun  13519  ixxss12  13523  ioodisj  13640  fz0fzelfz0  13795  mulexpz  14272  rpexpmord  14338  leexp1a  14345  expmulnbnd  14406  hashf1  14629  fi1uzind  14679  brfi1indALT  14682  swrdccat  14912  reuccatpfxs1  14924  abs3lem  15535  rexanre  15543  cau3lem  15551  limsupgre  15677  limsupbnd2  15679  o1lo1  15733  rlimclim1  15741  rlimclim  15742  rlimcn1  15784  rlimcn3  15786  o1of2  15809  o1rlimmul  15815  lo1add  15823  lo1mul  15824  isercolllem1  15861  climcau  15867  caucvgrlem  15869  caucvgb  15876  summolem2  15911  summo  15912  modfsummod  15990  o1fsum  16009  prodmolem2  16131  addmodlteqALT  16524  rpdvds  16864  isprm5  16912  isprm6  16919  pclem  17045  pcqmul  17060  pcexp  17066  pcneg  17081  pcprmpw2  17089  pcadd  17096  pcmpt  17099  4sqlem13  17164  vdwlem2  17189  vdwlem7  17194  vdwlem12  17199  ramval  17215  ramub2  17221  ramz2  17231  ramcl  17236  cshwshashlem2  17303  imasval  17712  imasdsval  17716  mreexexd  17851  acsfn  17862  issubc3  18053  idfucl  18085  funcres2c  18107  isnat  18154  fucpropd  18184  xpcval  18380  xpcco  18386  prfval  18402  evlf2  18421  evlfcl  18425  curf12  18430  curf1cl  18431  curf2  18432  curfcl  18435  curf2ndf  18450  hof2val  18459  hofcl  18462  hofpropd  18470  yonedalem4a  18478  yonedainv  18484  drsdirfi  18508  pospo  18546  poslubmo  18612  posglbmo  18613  isipodrs  18740  acsinfd  18759  chnccat  18829  chnpof1  18833  gsumvalx  18894  gsumpropd2lem  18897  mgmhmeql  18934  sgrppropd  18949  ismndd  18975  mndpropd  18980  mndpsuppss  18988  mhmeql  19051  mndind  19053  frmdup3lem  19091  mhmmnd  19303  issubg4  19385  ssnmz  19405  conjnmzb  19496  f1otrspeq  19691  psgneu  19750  pgpfi  19849  sylow2blem3  19866  slwhash  19868  fislw  19869  sylow3lem2  19872  lsmdisj2  19926  pj1eu  19940  efgredlem  19991  frgpuplem  20016  gexex  20097  frgpnabl  20119  dprdfadd  20266  dpjidcl  20304  pgpfac1lem3  20323  pgpfaclem3  20329  ablfac2  20335  ablsimpgcygd  20352  ablsimpgfind  20356  ablsimpgprmd  20361  rngpropd  20426  ringpropd  20549  imadrhmcl  21084  islmhm2  21343  lmhmpropd  21378  lbsextlem4  21469  prmidl2  21652  prmirredlem  21808  psgndiflemA  21937  lsmcss  22028  uvcf1  22128  frlmsslsp  22132  frlmup1  22134  assapropd  22209  psrval  22253  evlslem1  22421  mamucl  22746  mamuass  22747  mamudi  22748  mamudir  22749  mamuvs1  22750  mamuvs2  22751  mamulid  22786  mamurid  22787  dmatsubcl  22843  dmatmulcl  22845  scmatscm  22858  marrepval  22907  marepveval  22913  mdetunilem7  22963  gsummatr01lem4  23003  cpmatmcllem  23066  mat2pmatf1  23077  mat2pmatlin  23083  decpmatmul  23120  pm2mpmhmlem2  23167  chpidmat  23195  pptbas  23356  toponmre  23441  restbas  23506  iscncl  23617  cnrest2  23634  cnpdis  23641  lmcnp  23652  dishaus  23730  cmpcovf  23739  tgcmp  23749  dfconn2  23767  clsconn  23778  2ndcctbss  23804  dis2ndc  23809  1stccnp  23811  islly2  23833  cldllycmp  23844  locfincmp  23875  comppfsc  23881  kgentopon  23887  txcls  23953  ptpjopn  23961  dfac14  23967  xkoccn  23968  txcnp  23969  txcmpb  23993  txlm  23997  xkopt  24004  xkoco1cn  24006  xkoco2cn  24007  qtopcn  24063  qtoprest  24066  regr1lem2  24089  xkocnv  24163  qtophmeo  24166  fmfnfmlem4  24306  hausflim  24330  hauspwpwf1  24336  fclscmp  24379  alexsublem  24393  alexsubALTlem2  24397  alexsubALTlem3  24398  ptcmplem3  24403  ptcmplem4  24404  ptcmplem5  24405  cnextfun  24413  tmdgsum2  24445  symgtgp  24455  tsmsval2  24479  tsmsgsum  24488  utoptop  24583  ismet2  24682  blin  24770  metss2lem  24860  methaus  24869  met1stc  24870  met2ndci  24871  prdsxmslem2  24878  metcnp3  24889  metcnpi3  24895  metustto  24902  metustfbas  24906  nlmvscn  25036  nrginvrcn  25041  xrsxmet  25159  reconnlem1  25176  reconn  25178  xrge0tsms  25184  xmetdcn2  25187  metdscn  25206  addcnlem  25214  fsumcn  25221  cnheiborlem  25305  cnheibor  25306  bndth  25309  lebnum  25315  nmoleub2lem2  25467  ipcn  25597  iscmet3  25644  caubl  25659  rrxdstprj1  25760  minveclem3b  25779  minveclem7  25786  pjthlem2  25789  pmltpc  25801  volfiniun  25898  ioombl1  25913  dyadss  25945  dyaddisjlem  25946  dyadmax  25949  dyadmbllem  25950  opnmbllem  25952  itg1addlem2  26048  itg10a  26061  mbfi1fseqlem6  26071  itg2seq  26093  itg2monolem1  26101  itg2gt0  26111  itgfsum  26177  limcfval  26222  ellimc2  26227  ellimc3  26229  limcres  26236  limciun  26244  dvres  26261  dveflem  26329  rolle  26340  dvlip2  26345  c1liplem1  26346  dvgt0lem1  26352  dvgt0  26354  dvlt0  26355  dvne0  26361  dvfsumrlimge0  26380  ftc1lem6  26391  itgsubst  26399  mdegmullem  26426  ply1domn  26472  ply1divex  26485  fta1g  26518  fta1b  26520  plyf  26546  dgrlem  26578  coeid  26587  plydivalg  26650  aannenlem1  26685  aalioulem3  26691  aalioulem6  26694  abelthlem8  26796  efif1olem4  26903  chordthm  27195  xrlimcnp  27326  jensen  27346  lgamcvglem  27397  lgamcvg2  27412  sqf11  27496  fsumvma2  27571  perfectlem2  27587  lgsdilem  27681  lgsquad2lem2  27742  lgsquad3  27744  2sqlem5  27779  2sqlem9  27784  2sqb  27789  rpvmasumlem  27844  dchrisum0flb  27867  dchrisum0  27877  pntpbnd  27945  pntibndlem3  27949  pntleml  27968  flt4lem7  28019  nna4b4nsq  28020  nolt02o  28082  nosupbday  28092  nosupbnd2  28103  noinfbday  28107  noinfbnd2  28118  noetasuplem4  28123  noetainflem4  28127  noetalem1  28128  conway  28195  lesrec  28215  ltslpss  28324  addsprop  28392  bdayons  28692  n0fincut  28771  eucliddivs  28792  remulscllem2  28917  tgjustc1  28967  tgjustc2  28968  legov  29078  legtrid  29084  tglinethru  29134  tglineintmo  29140  tglnpt2  29151  mirreu3  29156  perpcom  29218  colperpexlem3  29238  mideu  29244  opphllem1  29253  hlpasch  29264  lnopp2hpgb  29271  trgcopy  29341  brcgr  29508  brbtwn2  29513  colinearalg  29518  axsegcon  29535  axeuclidlem  29570  axcontlem9  29580  ecgrtg  29591  elntg  29592  eengtrkg  29594  upgr1eopALT  29725  usgredg4  29828  subuhgr  29897  subumgr  29899  usgr2wspthon  30587  clwlkclwwlkf1  30631  eupth2lems  30869  n4cyclfrgr  30922  vacn  31326  blocni  31437  ubthlem3  31504  minvecolem7  31515  chocunii  31933  pjhthmo  31934  pjhthlem2  32024  kbass5  32752  mdsymlem5  33039  foresf1o  33172  fcobij  33382  xrofsup  33429  mgcoval  33617  mgcf1o  33634  xrge0tsmsd  33704  symgcntz  33716  archirngz  33820  archiabllem2a  33825  isarchiofld  33830  mplvrpmmhm  34248  constrelextdg2  34449  smatrcl  34498  reff  34541  ordtconnlem1  34626  qqhval2  34684  volmeas  34934  fiunelcarsg  35018  ballotlemfc0  35195  ballotlemfcc  35196  signstfvneq0  35271  j0ltalephlem  36007  derangenlem  36103  erdsze2lem1  36135  pconnconn  36163  connpconn  36167  cvxsconn  36175  cvmliftmolem2  36214  cvmliftmo  36216  cvmlift2lem10  36244  cvmlift2lem12  36246  cvmlift3lem7  36257  mrsubff1  36446  msubff1  36488  r1peuqusdeg1  36575  ifscgr  36987  cgrxfr  36998  btwnconn1lem13  37042  btwnconn1lem14  37043  outsideofeq  37073  ellines  37095  nadddilem4  37150  finminlem  37284  fnejoin2  37335  weiunso  37432  unbdqndv2  37555  irrdiff  38439  qdiff  38440  poimirlem13  38743  poimirlem14  38744  poimirlem32  38762  opnmbllem0  38766  mblfinlem3  38769  itg2addnclem  38781  itg2addnc  38784  ftc1cnnc  38802  upixp  38855  filbcmb  38866  sstotbnd2  38900  isbnd3  38910  prdsbnd2  38921  cntotbnd  38922  ismtyima  38929  bfp  38950  rrncmslem  38958  unichnidl  39157  lshpcmp  40237  islshpat  40266  lfl0f  40318  ishlat3N  40603  3dim1  40716  islvol5  40828  lvoli2  40830  lncvrelatN  41030  pclfinclN  41199  pexmidlem8N  41226  idltrn  41399  cdleme42keg  41735  cdleme42mgN  41737  cdlemf2  41811  cdlemg2cex  41840  trlcoat  41972  dihopelvalcpre  42497  dih1dimatlem  42578  dihjatcclem4  42670  lcfl7N  42750  lcfrlem9  42799  mapdh9a  43038  hdmapglem7  43178  aks4d1p8  43329  isprimroot  43335  evl1gprodd  43359  sticksstones11  43398  grpods  43436  aks5lem8  43443  renegeulemv  43612  sn-subeu  43671  remulinvcom  43677  imacrhmcl  43774  fidomncyc  43792  fsuppind  43811  fsuppssind  43814  mhpind  43815  prjspertr  43826  prjspreln0  43830  nacsfix  43916  mzpsubst  43952  mzpcompact2lem  43955  eldioph2lem2  43965  eldioph2  43966  eldioph2b  43967  diophin  43976  diophun  43977  irrapxlem3  44024  irrapxlem5  44026  pell1234qrreccl  44054  pell1234qrmulcl  44055  pell14qrdich  44069  pell1qrge1  44070  pell1qrgaplem  44073  monotuz  44141  acongtr  44178  acongrep  44180  jm2.23  44196  jm2.26a  44200  jm2.26lem3  44201  jm2.26  44202  jm2.27  44208  wepwsolem  44242  kelac1  44258  kercvrlsm  44278  hbtlem5  44322  hbt  44324  mpaaeu  44344  cantnfresb  44518  onmcl  44525  tfsconcatun  44531  tfsconcatfn  44532  tfsconcatfv1  44533  tfsconcatfv2  44534  naddcnff  44556  rfovcnvf1od  45196  mnurndlem1  45457  cncmpmax  46254  rfcnnnub  46258  disjxp1  46291  iccintsng  46740  fprodcn  46817  lptioo2  46848  lptioo1  46849  limclner  46866  stoweidlem31  47246  stoweidlem34  47249  stoweidlem35  47250  stoweidlem49  47264  stoweidlem59  47274  stoweidlem62  47277  fourierdlem60  47381  fourierdlem61  47382  fourierdlem87  47408  iundjiun  47675  ismeannd  47682  hoidmvle  47815  smfsuplem2  48027  2reu8i  48389  prproropf1olem2  48791  paireqne  48798  nprmmul2  48815  perfectALTVlem2  49025  mogoldbb  49088  bgoldbtbndlem2  49109  bgoldbtbndlem3  49110  grimedg  49238  grlimprclnbgrvtx  49302  scmsuppss  49688  lindslinindsimp2lem5  49779  elfzolborelfzop1  49836  elbigolo1  49874  itschlc0xyqsol1  50083  itschlc0xyqsol  50084  iccdisj  50217  toslat  50301  iinfssclem3  50375  iinfssc  50376  iinfsubc  50377  imasubc3  50477  upciclem4  50490  uppropd  50502  natoppf  50556  tposcurf1  50626  fuco22  50666  fuco22natlem  50672  functhinclem4  50787  arweuthinc  50869