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

Syntax hints:   → wi 4   ∧ wa 384

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

This theorem is referenced by:  disjxiun  4848  fsnex  6765  f1prex  6766  isotr  6813  weniso  6831  riota5f  6863  tfrlem9a  7721  oaass  7881  oeeui  7922  oaabs2  7965  resixpfo  8186  omxpenlem  8303  pw2f1olem  8306  fopwdom  8310  fofinf1o  8483  marypha1lem  8581  ordiso2  8662  oismo  8687  ixpiunwdom  8738  cantnf  8840  fseqenlem1  9133  iunfictbso  9223  dfac12lem2  9254  dfac12lem3  9255  infunsdom1  9323  infpssrlem5  9417  fin23lem24  9432  isf32lem2  9464  isf32lem4  9466  isf34lem4  9487  fin1a2lem12  9521  fin1a2lem13  9522  ttukeylem6  9624  fpwwe2lem12  9751  fpwwe2lem13  9752  fpwwe2  9753  winalim2  9806  wunex2  9848  tskord  9890  prlem934  10143  mulcmpblnr  10180  dedekind  10488  addid1  10504  cnegex  10505  negeu  10559  add20  10828  divdivdiv  11014  ltmul12a  11167  lemul12a  11169  lediv12a  11204  supaddc  11278  supmul1  11280  cru  11300  uzwo3  12005  xleadd1a  12304  xmullem  12315  xmulgt0  12334  xlemul1a  12339  ixxun  12412  ixxss12  12416  ioodisj  12528  fz0fzelfz0  12672  mulexpz  13126  leexp1a  13145  expmulnbnd  13222  hashf1  13461  fi1uzind  13499  brfi1indALT  13502  reuccats1  13707  abs3lem  14304  rexanre  14312  cau3lem  14320  limsupgre  14438  limsupbnd2  14440  o1lo1  14494  rlimclim1  14502  rlimclim  14503  rlimcn1  14545  rlimcn2  14547  o1of2  14569  o1rlimmul  14575  lo1add  14583  lo1mul  14584  isercolllem1  14621  climcau  14627  caucvgrlem  14629  caucvgb  14636  summolem2  14673  summo  14674  modfsummod  14751  o1fsum  14770  prodmolem2  14889  addmodlteqALT  15273  rpdvds  15595  isprm5  15639  isprm6  15646  pclem  15763  pcqmul  15778  pcexp  15784  pcneg  15798  pcprmpw2  15806  pcadd  15813  pcmpt  15816  4sqlem13  15881  vdwlem2  15906  vdwlem7  15911  vdwlem12  15916  ramval  15932  ramub2  15938  ramz2  15948  ramcl  15953  cshwshashlem2  16018  imasval  16379  imasdsval  16383  mreexexd  16516  acsfn  16527  issubc3  16716  idfucl  16748  funcres2c  16768  isnat  16814  fucpropd  16844  xpcval  17025  xpcco  17031  prfval  17047  evlf2  17066  evlfcl  17070  curf12  17075  curf1cl  17076  curf2  17077  curfcl  17080  curf2ndf  17095  hof2val  17104  hofcl  17107  hofpropd  17115  yonedalem4a  17123  yonedainv  17129  drsdirfi  17146  pospo  17181  poslubmo  17354  posglbmo  17355  isipodrs  17369  acsinfd  17388  gsumvalx  17478  gsumpropd2lem  17481  ismndd  17521  mndpropd  17524  mhmeql  17572  mrcmndind  17574  frmdup3lem  17611  mhmmnd  17745  issubg4  17818  ssnmz  17841  conjnmzb  17900  f1otrspeq  18071  psgneu  18130  pgpfi  18224  sylow2blem3  18241  slwhash  18243  fislw  18244  sylow3lem2  18247  lsmdisj2  18299  pj1eu  18313  efgredlem  18364  frgpuplem  18389  gexex  18460  frgpnabl  18482  dprdfadd  18624  dpjidcl  18662  pgpfac1lem3  18681  pgpfaclem3  18687  ablfac2  18693  ringpropd  18787  islmhm2  19248  lmhmpropd  19283  lbsextlem4  19373  assapropd  19539  psrval  19574  evlslem1  19726  prmirredlem  20052  psgndiflemA  20158  lsmcss  20250  uvcf1  20345  frlmsslsp  20349  frlmup1  20351  mamucl  20421  mamuass  20422  mamudi  20423  mamudir  20424  mamuvs1  20425  mamuvs2  20426  mamulid  20461  mamurid  20462  dmatsubcl  20519  dmatmulcl  20521  scmatscm  20534  marrepval  20583  marepveval  20589  mdetunilem7  20639  gsummatr01lem4  20680  cpmatmcllem  20740  mat2pmatf1  20751  mat2pmatlin  20757  decpmatmul  20794  pm2mpmhmlem2  20841  chpidmat  20869  pptbas  21030  toponmre  21115  restbas  21180  iscncl  21291  cnrest2  21308  cnpdis  21315  lmcnp  21326  dishaus  21404  cmpcovf  21412  tgcmp  21422  dfconn2  21440  clsconn  21451  2ndcctbss  21476  dis2ndc  21481  1stccnp  21483  islly2  21505  cldllycmp  21516  locfincmp  21547  comppfsc  21553  kgentopon  21559  txcls  21625  ptpjopn  21633  dfac14  21639  xkoccn  21640  txcnp  21641  txcmpb  21665  txlm  21669  xkopt  21676  xkoco1cn  21678  xkoco2cn  21679  qtopcn  21735  qtoprest  21738  regr1lem2  21761  xkocnv  21835  qtophmeo  21838  fmfnfmlem4  21978  hausflim  22002  hauspwpwf1  22008  fclscmp  22051  alexsublem  22065  alexsubALTlem2  22069  alexsubALTlem3  22070  ptcmplem3  22075  ptcmplem4  22076  ptcmplem5  22077  cnextfun  22085  tmdgsum2  22117  symgtgp  22122  tsmsval2  22150  tsmsgsum  22159  utoptop  22255  ismet2  22355  blin  22443  metss2lem  22533  methaus  22542  met1stc  22543  met2ndci  22544  prdsxmslem2  22551  metcnp3  22562  metcnpi3  22568  metustto  22575  metustfbas  22579  nlmvscn  22708  nrginvrcn  22713  xrsxmet  22829  reconnlem1  22846  reconn  22848  xrge0tsms  22854  xmetdcn2  22857  metdscn  22876  addcnlem  22884  fsumcn  22890  cnheiborlem  22970  cnheibor  22971  bndth  22974  lebnum  22980  nmoleub2lem2  23132  ipcn  23261  iscmet3  23308  caubl  23323  rrxdstprj1  23410  minveclem3b  23417  minveclem7  23424  pjthlem2  23427  pmltpc  23437  volfiniun  23534  ioombl1  23549  dyadss  23581  dyaddisjlem  23582  dyadmax  23585  dyadmbllem  23586  opnmbllem  23588  itg1addlem2  23684  itg10a  23697  mbfi1fseqlem6  23707  itg2seq  23729  itg2monolem1  23737  itg2gt0  23747  itgfsum  23813  limcfval  23856  ellimc2  23861  ellimc3  23863  limcres  23870  limciun  23878  dvres  23895  dveflem  23962  rolle  23973  dvlip2  23978  c1liplem1  23979  dvgt0lem1  23985  dvgt0  23987  dvlt0  23988  dvne0  23994  dvfsumrlimge0  24013  ftc1lem6  24024  itgsubst  24032  mdegmullem  24058  ply1domn  24103  ply1divex  24116  fta1g  24147  fta1b  24149  plyf  24174  dgrlem  24205  coeid  24214  plydivalg  24274  aannenlem1  24303  aalioulem3  24309  aalioulem6  24312  abelthlem8  24413  efif1olem4  24512  chordthm  24784  xrlimcnp  24915  jensen  24935  lgamcvglem  24986  lgamcvg2  25001  sqf11  25085  fsumvma2  25159  perfectlem2  25175  lgsdilem  25269  lgsquad2lem2  25330  lgsquad3  25332  2sqlem5  25367  2sqlem9  25372  2sqb  25377  rpvmasumlem  25396  dchrisum0flb  25419  dchrisum0  25429  pntpbnd  25497  pntibndlem3  25501  pntleml  25520  legov  25700  legtrid  25706  tglinethru  25751  tglnpt2  25756  tglineintmo  25757  mirreu3  25769  perpcom  25828  colperpexlem3  25844  mideu  25850  opphllem1  25859  hlpasch  25868  lnopp2hpgb  25875  trgcopy  25916  brcgr  26000  brbtwn2  26005  colinearalg  26010  axsegcon  26027  axeuclidlem  26062  axcontlem9  26072  ecgrtg  26083  elntg  26084  eengtrkg  26085  upgr1eopALT  26232  usgredg4  26330  subuhgr  26400  subumgr  26402  usgr2wspthon  27113  clwlkclwwlkf1  27159  eupth2lems  27417  n4cyclfrgr  27472  vacn  27883  blocni  27994  ubthlem3  28062  minvecolem7  28073  chocunii  28494  pjhthmo  28495  pjhthlem2  28585  kbass5  29313  mdsymlem5  29600  foresf1o  29674  fcobij  29833  xrofsup  29866  archirngz  30074  archiabllem2a  30079  xrge0tsmsd  30116  isarchiofld  30148  smatrcl  30193  reff  30237  ordtconnlem1  30301  qqhval2  30357  volmeas  30625  fiunelcarsg  30709  ballotlemfc0  30885  ballotlemfcc  30886  signstfvneq0  30980  derangenlem  31481  erdsze2lem1  31513  pconnconn  31541  connpconn  31545  cvxsconn  31553  cvmliftmolem2  31592  cvmliftmo  31594  cvmlift2lem10  31622  cvmlift2lem12  31624  cvmlift3lem7  31635  mrsubff1  31739  msubff1  31781  frpomin  32064  poseq  32079  nolt02o  32171  noprefixmo  32174  nosupbnd2  32188  noetalem3  32191  noetalem5  32193  conway  32236  slerec  32249  ifscgr  32477  cgrxfr  32488  btwnconn1lem13  32532  btwnconn1lem14  32533  outsideofeq  32563  ellines  32585  finminlem  32638  fnejoin2  32690  unbdqndv2  32824  poimirlem13  33737  poimirlem14  33738  poimirlem32  33756  opnmbllem0  33760  mblfinlem3  33763  itg2addnclem  33775  itg2addnc  33778  ftc1cnnc  33798  upixp  33838  filbcmb  33849  sstotbnd2  33886  isbnd3  33896  prdsbnd2  33907  cntotbnd  33908  ismtyima  33915  bfp  33936  rrncmslem  33944  unichnidl  34143  lshpcmp  34770  islshpat  34799  lfl0f  34851  ishlat3N  35136  3dim1  35249  islvol5  35361  lvoli2  35363  lncvrelatN  35563  pclfinclN  35732  pexmidlem8N  35759  idltrn  35932  cdleme42keg  36268  cdleme42mgN  36270  cdlemf2  36344  cdlemg2cex  36373  trlcoat  36505  dihopelvalcpre  37030  dih1dimatlem  37111  dihjatcclem4  37203  lcfl7N  37283  lcfrlem9  37332  mapdh9a  37571  hdmapglem7  37711  nacsfix  37778  mzpsubst  37814  mzpcompact2lem  37817  eldioph2lem2  37827  eldioph2  37828  eldioph2b  37829  diophin  37839  diophun  37840  irrapxlem3  37891  irrapxlem5  37893  pell1234qrreccl  37921  pell1234qrmulcl  37922  pell14qrdich  37936  pell1qrge1  37937  pell1qrgaplem  37940  monotuz  38008  rpexpmord  38015  acongtr  38047  acongrep  38049  jm2.23  38065  jm2.26a  38069  jm2.26lem3  38070  jm2.26  38071  jm2.27  38077  wepwsolem  38114  fnwe2lem2  38123  kelac1  38135  kercvrlsm  38155  hbtlem5  38200  hbt  38202  mpaaeu  38222  rfovcnvf1od  38799  cncmpmax  39686  rfcnnnub  39690  disjxp1  39732  iccintsng  40231  fprodcn  40313  lptioo2  40344  lptioo1  40345  limclner  40364  stoweidlem31  40728  stoweidlem34  40731  stoweidlem35  40732  stoweidlem49  40746  stoweidlem59  40756  stoweidlem62  40759  fourierdlem60  40863  fourierdlem61  40864  fourierdlem87  40890  iundjiun  41157  ismeannd  41164  hoidmvle  41297  smfsuplem2  41501  reuccatpfxs1  42010  perfectALTVlem2  42207  mogoldbb  42249  bgoldbtbndlem2  42270  bgoldbtbndlem3  42271  mgmhmeql  42372  mndpsuppss  42721  scmsuppss  42722  lindslinindsimp2lem5  42820  elfzolborelfzop1  42878  elbigolo1  42920