Theorem simplrr 777

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 726	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 206  df-an 396

This theorem is referenced by:  disjxiun  5139  frpomin  6340  fsnex  7286  f1prex  7287  isotr  7338  weniso  7356  riota5f  7399  frxp2  8143  frxp3  8150  xpord3pred  8151  poseq  8157  fprlem2  8300  tfrlem9a  8400  oaass  8575  oeeui  8616  oaabs2  8663  coflton  8685  cofon1  8686  naddssim  8699  resixpfo  8946  omxpenlem  9089  pw2f1olem  9092  fopwdom  9096  fofinf1o  9343  marypha1lem  9448  ordiso2  9530  oismo  9555  ixpiunwdom  9605  cantnf  9708  ttrclss  9735  fseqenlem1  10039  iunfictbso  10129  dfac12lem2  10159  dfac12lem3  10160  infunsdom1  10228  infpssrlem5  10322  fin23lem24  10337  isf32lem2  10369  isf32lem4  10371  isf34lem4  10392  fin1a2lem12  10426  fin1a2lem13  10427  ttukeylem6  10529  fpwwe2lem11  10656  fpwwe2lem12  10657  fpwwe2  10658  winalim2  10711  wunex2  10753  tskord  10795  prlem934  11048  mulcmpblnr  11086  dedekind  11399  addrid  11416  cnegex  11417  negeu  11472  add20  11748  divdivdiv  11937  ltmul12a  12092  lemul12a  12094  lediv12a  12129  supaddc  12203  supmul1  12205  cru  12226  uzwo3  12949  xleadd1a  13256  xmullem  13267  xmulgt0  13286  xlemul1a  13291  ixxun  13364  ixxss12  13368  ioodisj  13483  fz0fzelfz0  13631  mulexpz  14091  rpexpmord  14156  leexp1a  14163  expmulnbnd  14221  hashf1  14442  fi1uzind  14482  brfi1indALT  14485  swrdccat  14709  reuccatpfxs1  14721  abs3lem  15309  rexanre  15317  cau3lem  15325  limsupgre  15449  limsupbnd2  15451  o1lo1  15505  rlimclim1  15513  rlimclim  15514  rlimcn1  15556  rlimcn3  15558  o1of2  15581  o1rlimmul  15587  lo1add  15595  lo1mul  15596  isercolllem1  15635  climcau  15641  caucvgrlem  15643  caucvgb  15650  summolem2  15686  summo  15687  modfsummod  15764  o1fsum  15783  prodmolem2  15903  addmodlteqALT  16293  rpdvds  16622  isprm5  16669  isprm6  16676  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  17057  imasval  17484  imasdsval  17488  mreexexd  17619  acsfn  17630  issubc3  17826  idfucl  17858  funcres2c  17881  isnat  17928  fucpropd  17960  xpcval  18159  xpcco  18165  prfval  18181  evlf2  18201  evlfcl  18205  curf12  18210  curf1cl  18211  curf2  18212  curfcl  18215  curf2ndf  18230  hof2val  18239  hofcl  18242  hofpropd  18250  yonedalem4a  18258  yonedainv  18264  drsdirfi  18288  pospo  18328  poslubmo  18394  posglbmo  18395  isipodrs  18520  acsinfd  18539  gsumvalx  18627  gsumpropd2lem  18630  mgmhmeql  18667  sgrppropd  18682  ismndd  18707  mndpropd  18710  mhmeql  18769  mndind  18771  frmdup3lem  18809  mhmmnd  19011  issubg4  19091  ssnmz  19112  conjnmzb  19198  f1otrspeq  19393  psgneu  19452  pgpfi  19551  sylow2blem3  19568  slwhash  19570  fislw  19571  sylow3lem2  19574  lsmdisj2  19628  pj1eu  19642  efgredlem  19693  frgpuplem  19718  gexex  19799  frgpnabl  19821  dprdfadd  19968  dpjidcl  20006  pgpfac1lem3  20025  pgpfaclem3  20031  ablfac2  20037  ablsimpgcygd  20054  ablsimpgfind  20058  ablsimpgprmd  20063  rngpropd  20105  ringpropd  20213  imadrhmcl  20674  islmhm2  20912  lmhmpropd  20947  lbsextlem4  21038  prmirredlem  21385  psgndiflemA  21520  lsmcss  21611  uvcf1  21713  frlmsslsp  21717  frlmup1  21719  assapropd  21792  psrval  21835  evlslem1  22015  mamucl  22288  mamuass  22289  mamudi  22290  mamudir  22291  mamuvs1  22292  mamuvs2  22293  mamulid  22330  mamurid  22331  dmatsubcl  22387  dmatmulcl  22389  scmatscm  22402  marrepval  22451  marepveval  22457  mdetunilem7  22507  gsummatr01lem4  22547  cpmatmcllem  22607  mat2pmatf1  22618  mat2pmatlin  22624  decpmatmul  22661  pm2mpmhmlem2  22708  chpidmat  22736  pptbas  22898  toponmre  22984  restbas  23049  iscncl  23160  cnrest2  23177  cnpdis  23184  lmcnp  23195  dishaus  23273  cmpcovf  23282  tgcmp  23292  dfconn2  23310  clsconn  23321  2ndcctbss  23346  dis2ndc  23351  1stccnp  23353  islly2  23375  cldllycmp  23386  locfincmp  23417  comppfsc  23423  kgentopon  23429  txcls  23495  ptpjopn  23503  dfac14  23509  xkoccn  23510  txcnp  23511  txcmpb  23535  txlm  23539  xkopt  23546  xkoco1cn  23548  xkoco2cn  23549  qtopcn  23605  qtoprest  23608  regr1lem2  23631  xkocnv  23705  qtophmeo  23708  fmfnfmlem4  23848  hausflim  23872  hauspwpwf1  23878  fclscmp  23921  alexsublem  23935  alexsubALTlem2  23939  alexsubALTlem3  23940  ptcmplem3  23945  ptcmplem4  23946  ptcmplem5  23947  cnextfun  23955  tmdgsum2  23987  symgtgp  23997  tsmsval2  24021  tsmsgsum  24030  utoptop  24126  ismet2  24226  blin  24314  metss2lem  24407  methaus  24416  met1stc  24417  met2ndci  24418  prdsxmslem2  24425  metcnp3  24436  metcnpi3  24442  metustto  24449  metustfbas  24453  nlmvscn  24591  nrginvrcn  24596  xrsxmet  24712  reconnlem1  24729  reconn  24731  xrge0tsms  24737  xmetdcn2  24740  metdscn  24759  addcnlem  24767  fsumcn  24775  cnheiborlem  24867  cnheibor  24868  bndth  24871  lebnum  24877  nmoleub2lem2  25030  ipcn  25161  iscmet3  25208  caubl  25223  rrxdstprj1  25324  minveclem3b  25343  minveclem7  25350  pjthlem2  25353  pmltpc  25366  volfiniun  25463  ioombl1  25478  dyadss  25510  dyaddisjlem  25511  dyadmax  25514  dyadmbllem  25515  opnmbllem  25517  itg1addlem2  25613  itg10a  25627  mbfi1fseqlem6  25637  itg2seq  25659  itg2monolem1  25667  itg2gt0  25677  itgfsum  25743  limcfval  25788  ellimc2  25793  ellimc3  25795  limcres  25802  limciun  25810  dvres  25827  dveflem  25898  rolle  25909  dvlip2  25915  c1liplem1  25916  dvgt0lem1  25922  dvgt0  25924  dvlt0  25925  dvne0  25931  dvfsumrlimge0  25952  ftc1lem6  25963  itgsubst  25971  mdegmullem  26001  ply1domn  26046  ply1divex  26059  fta1g  26091  fta1b  26093  plyf  26119  dgrlem  26150  coeid  26159  plydivalg  26221  aannenlem1  26250  aalioulem3  26256  aalioulem6  26259  abelthlem8  26363  efif1olem4  26466  chordthm  26756  xrlimcnp  26887  jensen  26908  lgamcvglem  26959  lgamcvg2  26974  sqf11  27058  fsumvma2  27134  perfectlem2  27150  lgsdilem  27244  lgsquad2lem2  27305  lgsquad3  27307  2sqlem5  27342  2sqlem9  27347  2sqb  27352  rpvmasumlem  27407  dchrisum0flb  27430  dchrisum0  27440  pntpbnd  27508  pntibndlem3  27512  pntleml  27531  nolt02o  27615  nosupbday  27625  nosupbnd2  27636  noinfbday  27640  noinfbnd2  27651  noetasuplem4  27656  noetainflem4  27660  noetalem1  27661  conway  27719  slerec  27739  sltlpss  27820  addsprop  27880  remulscllem2  28216  tgjustc1  28266  tgjustc2  28267  legov  28376  legtrid  28382  tglinethru  28427  tglnpt2  28432  tglineintmo  28433  mirreu3  28445  perpcom  28504  colperpexlem3  28523  mideu  28529  opphllem1  28538  hlpasch  28547  lnopp2hpgb  28554  trgcopy  28595  brcgr  28698  brbtwn2  28703  colinearalg  28708  axsegcon  28725  axeuclidlem  28760  axcontlem9  28770  ecgrtg  28781  elntg  28782  eengtrkg  28784  upgr1eopALT  28917  usgredg4  29017  subuhgr  29086  subumgr  29088  usgr2wspthon  29763  clwlkclwwlkf1  29807  eupth2lems  30035  n4cyclfrgr  30088  vacn  30491  blocni  30602  ubthlem3  30669  minvecolem7  30680  chocunii  31098  pjhthmo  31099  pjhthlem2  31189  kbass5  31917  mdsymlem5  32204  foresf1o  32286  fcobij  32488  xrofsup  32521  mgcoval  32695  mgcf1o  32712  xrge0tsmsd  32749  symgcntz  32786  archirngz  32875  archiabllem2a  32880  isarchiofld  32972  prmidl2  33092  smatrcl  33333  reff  33376  ordtconnlem1  33461  qqhval2  33519  volmeas  33786  fiunelcarsg  33872  ballotlemfc0  34048  ballotlemfcc  34049  signstfvneq0  34140  derangenlem  34717  erdsze2lem1  34749  pconnconn  34777  connpconn  34781  cvxsconn  34789  cvmliftmolem2  34828  cvmliftmo  34830  cvmlift2lem10  34858  cvmlift2lem12  34860  cvmlift3lem7  34871  mrsubff1  35060  msubff1  35102  ifscgr  35576  cgrxfr  35587  btwnconn1lem13  35631  btwnconn1lem14  35632  outsideofeq  35662  ellines  35684  finminlem  35738  fnejoin2  35789  unbdqndv2  35922  irrdiff  36741  poimirlem13  37041  poimirlem14  37042  poimirlem32  37060  opnmbllem0  37064  mblfinlem3  37067  itg2addnclem  37079  itg2addnc  37082  ftc1cnnc  37100  upixp  37137  filbcmb  37148  sstotbnd2  37182  isbnd3  37192  prdsbnd2  37203  cntotbnd  37204  ismtyima  37211  bfp  37232  rrncmslem  37240  unichnidl  37439  lshpcmp  38397  islshpat  38426  lfl0f  38478  ishlat3N  38763  3dim1  38877  islvol5  38989  lvoli2  38991  lncvrelatN  39191  pclfinclN  39360  pexmidlem8N  39387  idltrn  39560  cdleme42keg  39896  cdleme42mgN  39898  cdlemf2  39972  cdlemg2cex  40001  trlcoat  40133  dihopelvalcpre  40658  dih1dimatlem  40739  dihjatcclem4  40831  lcfl7N  40911  lcfrlem9  40960  mapdh9a  41199  hdmapglem7  41339  aks4d1p8  41495  isprimroot  41501  evl1gprodd  41521  sticksstones11  41560  imacrhmcl  41673  fsuppind  41745  fsuppssind  41748  mhpind  41749  renegeulemv  41845  sn-subeu  41903  remulinvcom  41909  sn-itrere  41943  sn-retire  41944  prjspertr  41951  prjspreln0  41955  flt4lem7  42005  nna4b4nsq  42006  nacsfix  42054  mzpsubst  42090  mzpcompact2lem  42093  eldioph2lem2  42103  eldioph2  42104  eldioph2b  42105  diophin  42114  diophun  42115  irrapxlem3  42166  irrapxlem5  42168  pell1234qrreccl  42196  pell1234qrmulcl  42197  pell14qrdich  42211  pell1qrge1  42212  pell1qrgaplem  42215  monotuz  42284  acongtr  42321  acongrep  42323  jm2.23  42339  jm2.26a  42343  jm2.26lem3  42344  jm2.26  42345  jm2.27  42351  wepwsolem  42388  fnwe2lem2  42397  kelac1  42409  kercvrlsm  42429  hbtlem5  42474  hbt  42476  mpaaeu  42496  cantnfresb  42676  onmcl  42683  tfsconcatun  42689  tfsconcatfn  42690  tfsconcatfv1  42691  tfsconcatfv2  42692  naddcnff  42714  rfovcnvf1od  43357  mnurndlem1  43641  cncmpmax  44317  rfcnnnub  44321  disjxp1  44356  iccintsng  44831  fprodcn  44911  lptioo2  44942  lptioo1  44943  limclner  44962  stoweidlem31  45342  stoweidlem34  45345  stoweidlem35  45346  stoweidlem49  45360  stoweidlem59  45370  stoweidlem62  45373  fourierdlem60  45477  fourierdlem61  45478  fourierdlem87  45504  iundjiun  45771  ismeannd  45778  hoidmvle  45911  smfsuplem2  46123  2reu8i  46416  prproropf1olem2  46767  paireqne  46774  perfectALTVlem2  46985  mogoldbb  47048  bgoldbtbndlem2  47069  bgoldbtbndlem3  47070  uspgrimprop  47094  mndpsuppss  47358  scmsuppss  47359  lindslinindsimp2lem5  47453  elfzolborelfzop1  47510  elbigolo1  47553  itschlc0xyqsol1  47762  itschlc0xyqsol  47763  iccdisj  47840  toslat  47916  functhinclem4  47973