Theorem simplrr 797

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  disjxiun  4579  disjxiunOLD  4580  fsnex  6438  f1prex  6439  isotr  6486  weniso  6504  riota5f  6535  tfrlem9a  7369  oaass  7528  oeeui  7569  oaabs2  7612  resixpfo  7832  omxpenlem  7946  pw2f1olem  7949  fopwdom  7953  fofinf1o  8126  marypha1lem  8222  ordiso2  8303  oismo  8328  ixpiunwdom  8379  cantnf  8473  fseqenlem1  8730  iunfictbso  8820  dfac12lem2  8849  dfac12lem3  8850  infunsdom1  8918  infpssrlem5  9012  fin23lem24  9027  isf32lem2  9059  isf32lem4  9061  isf34lem4  9082  fin1a2lem12  9116  fin1a2lem13  9117  ttukeylem6  9219  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  winalim2  9397  wunex2  9439  tskord  9481  prlem934  9734  mulcmpblnr  9771  dedekind  10079  addid1  10095  cnegex  10096  negeu  10150  add20  10419  divdivdiv  10605  ltmul12a  10758  lemul12a  10760  lediv12a  10795  supaddc  10867  supmul1  10869  cru  10889  uzwo3  11659  xleadd1a  11955  xmullem  11966  xmulgt0  11985  xlemul1a  11990  ixxun  12062  ixxss12  12066  ioodisj  12173  fz0fzelfz0  12314  mulexpz  12762  leexp1a  12781  expmulnbnd  12858  hashf1  13098  fi1uzind  13134  brfi1indALT  13137  fi1uzindOLD  13140  brfi1indALTOLD  13143  reuccats1  13332  abs3lem  13926  rexanre  13934  cau3lem  13942  limsupgre  14060  limsupbnd2  14062  o1lo1  14116  rlimclim1  14124  rlimclim  14125  rlimcn1  14167  rlimcn2  14169  o1of2  14191  o1rlimmul  14197  lo1add  14205  lo1mul  14206  isercolllem1  14243  climcau  14249  caucvgrlem  14251  caucvgb  14258  summolem2  14294  summo  14295  modfsummod  14367  o1fsum  14386  prodmolem2  14504  addmodlteqALT  14885  rpdvds  15212  isprm5  15257  isprm6  15264  pclem  15381  pcqmul  15396  pcexp  15402  pcneg  15416  pcprmpw2  15424  pcadd  15431  pcmpt  15434  4sqlem13  15499  vdwlem2  15524  vdwlem7  15529  vdwlem12  15534  ramval  15550  ramub2  15556  ramz2  15566  ramcl  15571  cshwshashlem2  15641  imasval  15994  imasdsval  15998  mreexexd  16131  mreexexdOLD  16132  acsfn  16143  issubc3  16332  idfucl  16364  funcres2c  16384  isnat  16430  fucpropd  16460  xpcval  16640  xpcco  16646  prfval  16662  evlf2  16681  evlfcl  16685  curf12  16690  curf1cl  16691  curf2  16692  curfcl  16695  curf2ndf  16710  hof2val  16719  hofcl  16722  hofpropd  16730  yonedalem4a  16738  yonedainv  16744  drsdirfi  16761  pospo  16796  poslubmo  16969  posglbmo  16970  isipodrs  16984  acsinfd  17003  gsumvalx  17093  gsumpropd2lem  17096  ismndd  17136  mndpropd  17139  mhmeql  17187  mrcmndind  17189  frmdup3lem  17226  mhmmnd  17360  issubg4  17436  ssnmz  17459  conjnmzb  17518  f1otrspeq  17690  psgneu  17749  pgpfi  17843  sylow2blem3  17860  slwhash  17862  fislw  17863  sylow3lem2  17866  lsmdisj2  17918  pj1eu  17932  efgredlem  17983  frgpuplem  18008  gexex  18079  frgpnabl  18101  dprdfadd  18242  dpjidcl  18280  pgpfac1lem3  18299  pgpfaclem3  18305  ablfac2  18311  ringpropd  18405  islmhm2  18859  lmhmpropd  18894  lbsextlem4  18982  assapropd  19148  psrval  19183  evlslem1  19336  prmirredlem  19660  psgndiflemA  19766  lsmcss  19855  uvcf1  19950  frlmsslsp  19954  frlmup1  19956  mamucl  20026  mamuass  20027  mamudi  20028  mamudir  20029  mamuvs1  20030  mamuvs2  20031  mamulid  20066  mamurid  20067  dmatsubcl  20123  dmatmulcl  20125  scmatscm  20138  marrepval  20187  marepveval  20193  mdetunilem7  20243  gsummatr01lem4  20283  cpmatmcllem  20342  mat2pmatf1  20353  mat2pmatlin  20359  decpmatmul  20396  pm2mpmhmlem2  20443  chpidmat  20471  pptbas  20622  toponmre  20707  restbas  20772  iscncl  20883  cnrest2  20900  cnpdis  20907  lmcnp  20918  dishaus  20996  cmpcovf  21004  tgcmp  21014  dfcon2  21032  clscon  21043  2ndcctbss  21068  dis2ndc  21073  1stccnp  21075  islly2  21097  cldllycmp  21108  locfincmp  21139  comppfsc  21145  kgentopon  21151  txcls  21217  ptpjopn  21225  dfac14  21231  xkoccn  21232  txcnp  21233  txcmpb  21257  txlm  21261  xkopt  21268  xkoco1cn  21270  xkoco2cn  21271  qtopcn  21327  qtoprest  21330  regr1lem2  21353  xkocnv  21427  qtophmeo  21430  fmfnfmlem4  21571  hausflim  21595  hauspwpwf1  21601  fclscmp  21644  alexsublem  21658  alexsubALTlem2  21662  alexsubALTlem3  21663  ptcmplem3  21668  ptcmplem4  21669  ptcmplem5  21670  cnextfun  21678  tmdgsum2  21710  symgtgp  21715  tsmsval2  21743  tsmsgsum  21752  utoptop  21848  ismet2  21948  blin  22036  metss2lem  22126  methaus  22135  met1stc  22136  met2ndci  22137  prdsxmslem2  22144  metcnp3  22155  metcnpi3  22161  metustto  22168  metustfbas  22172  nlmvscn  22301  nrginvrcn  22306  xrsxmet  22420  reconnlem1  22437  reconn  22439  xrge0tsms  22445  xmetdcn2  22448  metdscn  22467  addcnlem  22475  fsumcn  22481  cnheiborlem  22561  cnheibor  22562  bndth  22565  lebnum  22571  nmoleub2lem2  22724  ipcn  22853  iscmet3  22899  caubl  22914  rrxdstprj1  23000  minveclem3b  23007  minveclem7  23014  pjthlem2  23017  pmltpc  23026  volfiniun  23122  ioombl1  23137  dyadss  23168  dyaddisjlem  23169  dyadmax  23172  dyadmbllem  23173  opnmbllem  23175  itg1addlem2  23270  itg10a  23283  mbfi1fseqlem6  23293  itg2seq  23315  itg2monolem1  23323  itg2gt0  23333  itgfsum  23399  limcfval  23442  ellimc2  23447  ellimc3  23449  limcres  23456  limciun  23464  dvres  23481  dveflem  23546  rolle  23557  dvlip2  23562  c1liplem1  23563  dvgt0lem1  23569  dvgt0  23571  dvlt0  23572  dvne0  23578  dvfsumrlimge0  23597  ftc1lem6  23608  itgsubst  23616  mdegmullem  23642  ply1domn  23687  ply1divex  23700  fta1g  23731  fta1b  23733  plyf  23758  dgrlem  23789  coeid  23798  plydivalg  23858  aannenlem1  23887  aalioulem3  23893  aalioulem6  23896  abelthlem8  23997  efif1olem4  24095  chordthm  24364  xrlimcnp  24495  jensen  24515  lgamcvglem  24566  lgamcvg2  24581  sqf11  24665  fsumvma2  24739  perfectlem2  24755  lgsdilem  24849  lgsquad2lem2  24910  lgsquad3  24912  2sqlem5  24947  2sqlem9  24952  2sqb  24957  rpvmasumlem  24976  dchrisum0flb  24999  dchrisum0  25009  pntpbnd  25077  pntibndlem3  25081  pntleml  25100  legov  25280  legtrid  25286  tglinethru  25331  tglnpt2  25336  tglineintmo  25337  mirreu3  25349  perpcom  25408  colperpexlem3  25424  mideu  25430  opphllem1  25439  hlpasch  25448  lnopp2hpgb  25455  trgcopy  25496  brcgr  25580  brbtwn2  25585  colinearalg  25590  axsegcon  25607  axeuclidlem  25642  axcontlem9  25652  ecgrtg  25663  elntg  25664  eengtrkg  25665  upgr1eopALT  25783  cusgrarn  25988  usgrasscusgra  26011  4cycl4dv4e  26196  wwlkext2clwwlk  26331  usg2spthonot1  26417  usgfidegfi  26437  eupath2  26507  usg2spot2nb  26592  numclwwlk6  26640  vacn  26933  blocni  27044  ubthlem3  27112  minvecolem7  27123  chocunii  27544  pjhthmo  27545  pjhthlem2  27635  kbass5  28363  mdsymlem5  28650  foresf1o  28727  fcobij  28888  xrofsup  28923  archirngz  29074  archiabllem2a  29079  xrge0tsmsd  29116  isarchiofld  29148  smatrcl  29190  reff  29234  ordtconlem1  29298  qqhval2  29354  volmeas  29621  fiunelcarsg  29705  ballotlemfc0  29881  ballotlemfcc  29882  signstfvneq0  29975  derangenlem  30407  erdsze2lem1  30439  pconcon  30467  conpcon  30471  cvxscon  30479  cvmliftmolem2  30518  cvmliftmo  30520  cvmlift2lem10  30548  cvmlift2lem12  30550  cvmlift3lem7  30561  mrsubff1  30665  msubff1  30707  poseq  30994  ifscgr  31321  cgrxfr  31332  btwnconn1lem13  31376  btwnconn1lem14  31377  outsideofeq  31407  ellines  31429  finminlem  31482  fnejoin2  31534  unbdqndv2  31672  poimirlem13  32592  poimirlem14  32593  poimirlem32  32611  opnmbllem0  32615  mblfinlem3  32618  itg2addnclem  32631  itg2addnc  32634  ftc1cnnc  32654  upixp  32694  filbcmb  32705  sstotbnd2  32743  isbnd3  32753  prdsbnd2  32764  cntotbnd  32765  ismtyima  32772  bfp  32793  rrncmslem  32801  unichnidl  33000  lshpcmp  33293  islshpat  33322  lfl0f  33374  ishlat3N  33659  3dim1  33771  islvol5  33883  lvoli2  33885  lncvrelatN  34085  pclfinclN  34254  pexmidlem8N  34281  idltrn  34454  cdleme42keg  34792  cdleme42mgN  34794  cdlemf2  34868  cdlemg2cex  34897  trlcoat  35029  dihopelvalcpre  35555  dih1dimatlem  35636  dihjatcclem4  35728  lcfl7N  35808  lcfrlem9  35857  mapdh9a  36097  hdmapglem7  36239  nacsfix  36293  mzpsubst  36329  mzpcompact2lem  36332  eldioph2lem2  36342  eldioph2  36343  eldioph2b  36344  diophin  36354  diophun  36355  irrapxlem3  36406  irrapxlem5  36408  pell1234qrreccl  36436  pell1234qrmulcl  36437  pell14qrdich  36451  pell1qrge1  36452  pell1qrgaplem  36455  monotuz  36524  rpexpmord  36531  acongtr  36563  acongrep  36565  jm2.23  36581  jm2.26a  36585  jm2.26lem3  36586  jm2.26  36587  jm2.27  36593  wepwsolem  36630  fnwe2lem2  36639  kelac1  36651  kercvrlsm  36671  hbtlem5  36717  hbt  36719  mpaaeu  36739  rfovcnvf1od  37318  cncmpmax  38214  rfcnnnub  38218  disjxp1  38263  iccintsng  38596  fprodcn  38667  lptioo2  38698  lptioo1  38699  limclner  38718  stoweidlem31  38924  stoweidlem34  38927  stoweidlem35  38928  stoweidlem49  38942  stoweidlem59  38952  stoweidlem62  38955  fourierdlem60  39059  fourierdlem61  39060  fourierdlem87  39086  iundjiun  39353  ismeannd  39360  hoidmvle  39490  perfectALTVlem2  40165  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  reuccatpfxs1  40297  usgredg4  40444  subuhgr  40510  subumgr  40512  usgr2wspthon  41168  eupth2lems  41406  n4cyclfrgr  41461  frgr2wwlkeu  41492  mgmhmeql  41593  mndpsuppss  41946  scmsuppss  41947  lindslinindsimp2lem5  42045  elfzolborelfzop1  42103  elbigolo1  42149