Theorem simplrr 789

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  disjxiun  5110  frpomin  6344  fsnex  7284  f1prex  7285  isotr  7337  weniso  7355  riota5f  7398  frxp2  8142  frxp3  8149  xpord3pred  8150  poseq  8156  fprlem2  8300  tfrlem9a  8375  oaass  8548  oeeui  8590  oaabs2  8637  coflton  8659  cofon1  8660  naddssim  8674  resixpfo  8936  omxpenlem  9068  pw2f1olem  9071  fopwdom  9075  fofinf1o  9291  marypha1lem  9395  ordiso2  9479  oismo  9504  ixpiunwdom  9554  cantnf  9664  ttrclss  9691  fseqenlem1  10010  iunfictbso  10100  dfac12lem2  10130  dfac12lem3  10131  infunsdom1  10197  infpssrlem5  10293  fin23lem24  10308  isf32lem2  10340  isf32lem4  10342  isf34lem4  10363  fin1a2lem12  10397  fin1a2lem13  10398  ttukeylem6  10500  fpwwe2lem11  10628  fpwwe2lem12  10629  fpwwe2  10630  winalim2  10683  wunex2  10725  tskord  10767  prlem934  11020  mulcmpblnr  11058  dedekind  11375  addrid  11392  cnegex  11393  negeu  11449  add20  11728  divdivdiv  11918  ltmul12a  12073  lemul12a  12075  lediv12a  12110  supaddc  12184  supmul1  12186  cru  12212  uzwo3  12969  xleadd1a  13281  xmullem  13292  xmulgt0  13311  xlemul1a  13316  ixxun  13390  ixxss12  13394  ioodisj  13511  fz0fzelfz0  13664  mulexpz  14140  rpexpmord  14206  leexp1a  14213  expmulnbnd  14273  hashf1  14496  fi1uzind  14546  brfi1indALT  14549  swrdccat  14774  reuccatpfxs1  14786  abs3lem  15392  rexanre  15400  cau3lem  15408  limsupgre  15534  limsupbnd2  15536  o1lo1  15590  rlimclim1  15598  rlimclim  15599  rlimcn1  15641  rlimcn3  15643  o1of2  15666  o1rlimmul  15672  lo1add  15680  lo1mul  15681  isercolllem1  15718  climcau  15724  caucvgrlem  15726  caucvgb  15733  summolem2  15769  summo  15770  modfsummod  15848  o1fsum  15867  prodmolem2  15991  addmodlteqALT  16385  rpdvds  16720  isprm5  16768  isprm6  16775  pclem  16900  pcqmul  16915  pcexp  16921  pcneg  16936  pcprmpw2  16944  pcadd  16951  pcmpt  16954  4sqlem13  17019  vdwlem2  17044  vdwlem7  17049  vdwlem12  17054  ramval  17070  ramub2  17076  ramz2  17086  ramcl  17091  cshwshashlem2  17158  imasval  17567  imasdsval  17571  mreexexd  17706  acsfn  17717  issubc3  17908  idfucl  17940  funcres2c  17962  isnat  18009  fucpropd  18039  xpcval  18235  xpcco  18241  prfval  18257  evlf2  18276  evlfcl  18280  curf12  18285  curf1cl  18286  curf2  18287  curfcl  18290  curf2ndf  18305  hof2val  18314  hofcl  18317  hofpropd  18325  yonedalem4a  18333  yonedainv  18339  drsdirfi  18363  pospo  18401  poslubmo  18467  posglbmo  18468  isipodrs  18595  acsinfd  18614  chnccat  18684  chnpof1  18688  gsumvalx  18736  gsumpropd2lem  18739  mgmhmeql  18776  sgrppropd  18791  ismndd  18816  mndpropd  18819  mndpsuppss  18825  mhmeql  18887  mndind  18889  frmdup3lem  18927  mhmmnd  19132  issubg4  19214  ssnmz  19234  conjnmzb  19325  f1otrspeq  19519  psgneu  19578  pgpfi  19677  sylow2blem3  19694  slwhash  19696  fislw  19697  sylow3lem2  19700  lsmdisj2  19754  pj1eu  19768  efgredlem  19819  frgpuplem  19844  gexex  19925  frgpnabl  19947  dprdfadd  20094  dpjidcl  20132  pgpfac1lem3  20151  pgpfaclem3  20157  ablfac2  20163  ablsimpgcygd  20180  ablsimpgfind  20184  ablsimpgprmd  20189  rngpropd  20254  ringpropd  20373  imadrhmcl  20880  islmhm2  21139  lmhmpropd  21174  lbsextlem4  21265  prmidl2  21439  prmirredlem  21593  psgndiflemA  21722  lsmcss  21813  uvcf1  21913  frlmsslsp  21917  frlmup1  21919  assapropd  21992  psrval  22036  evlslem1  22204  mamucl  22529  mamuass  22530  mamudi  22531  mamudir  22532  mamuvs1  22533  mamuvs2  22534  mamulid  22569  mamurid  22570  dmatsubcl  22626  dmatmulcl  22628  scmatscm  22641  marrepval  22690  marepveval  22696  mdetunilem7  22746  gsummatr01lem4  22786  cpmatmcllem  22846  mat2pmatf1  22857  mat2pmatlin  22863  decpmatmul  22900  pm2mpmhmlem2  22947  chpidmat  22975  pptbas  23136  toponmre  23221  restbas  23286  iscncl  23397  cnrest2  23414  cnpdis  23421  lmcnp  23432  dishaus  23510  cmpcovf  23519  tgcmp  23529  dfconn2  23547  clsconn  23558  2ndcctbss  23583  dis2ndc  23588  1stccnp  23590  islly2  23612  cldllycmp  23623  locfincmp  23654  comppfsc  23660  kgentopon  23666  txcls  23732  ptpjopn  23740  dfac14  23746  xkoccn  23747  txcnp  23748  txcmpb  23772  txlm  23776  xkopt  23783  xkoco1cn  23785  xkoco2cn  23786  qtopcn  23842  qtoprest  23845  regr1lem2  23868  xkocnv  23942  qtophmeo  23945  fmfnfmlem4  24085  hausflim  24109  hauspwpwf1  24115  fclscmp  24158  alexsublem  24172  alexsubALTlem2  24176  alexsubALTlem3  24177  ptcmplem3  24182  ptcmplem4  24183  ptcmplem5  24184  cnextfun  24192  tmdgsum2  24224  symgtgp  24234  tsmsval2  24258  tsmsgsum  24267  utoptop  24362  ismet2  24461  blin  24549  metss2lem  24639  methaus  24648  met1stc  24649  met2ndci  24650  prdsxmslem2  24657  metcnp3  24668  metcnpi3  24674  metustto  24681  metustfbas  24685  nlmvscn  24815  nrginvrcn  24820  xrsxmet  24938  reconnlem1  24955  reconn  24957  xrge0tsms  24963  xmetdcn2  24966  metdscn  24985  addcnlem  24993  fsumcn  25000  cnheiborlem  25084  cnheibor  25085  bndth  25088  lebnum  25094  nmoleub2lem2  25246  ipcn  25376  iscmet3  25423  caubl  25438  rrxdstprj1  25539  minveclem3b  25558  minveclem7  25565  pjthlem2  25568  pmltpc  25580  volfiniun  25677  ioombl1  25692  dyadss  25724  dyaddisjlem  25725  dyadmax  25728  dyadmbllem  25729  opnmbllem  25731  itg1addlem2  25827  itg10a  25840  mbfi1fseqlem6  25850  itg2seq  25872  itg2monolem1  25880  itg2gt0  25890  itgfsum  25957  limcfval  26002  ellimc2  26007  ellimc3  26009  limcres  26016  limciun  26024  dvres  26041  dveflem  26109  rolle  26120  dvlip2  26125  c1liplem1  26126  dvgt0lem1  26132  dvgt0  26134  dvlt0  26135  dvne0  26141  dvfsumrlimge0  26160  ftc1lem6  26171  itgsubst  26179  mdegmullem  26206  ply1domn  26252  ply1divex  26265  fta1g  26298  fta1b  26300  plyf  26326  dgrlem  26357  coeid  26366  plydivalg  26431  aannenlem1  26460  aalioulem3  26466  aalioulem6  26469  abelthlem8  26570  efif1olem4  26678  chordthm  26970  xrlimcnp  27101  jensen  27121  lgamcvglem  27172  lgamcvg2  27187  sqf11  27271  fsumvma2  27346  perfectlem2  27362  lgsdilem  27456  lgsquad2lem2  27517  lgsquad3  27519  2sqlem5  27554  2sqlem9  27559  2sqb  27564  rpvmasumlem  27619  dchrisum0flb  27642  dchrisum0  27652  pntpbnd  27720  pntibndlem3  27724  pntleml  27743  nolt02o  27827  nosupbday  27837  nosupbnd2  27848  noinfbday  27852  noinfbnd2  27863  noetasuplem4  27868  noetainflem4  27872  noetalem1  27873  conway  27940  lesrec  27960  ltslpss  28069  addsprop  28137  bdayons  28437  n0fincut  28516  eucliddivs  28537  remulscllem2  28662  tgjustc1  28712  tgjustc2  28713  legov  28822  legtrid  28828  tglinethru  28873  tglineintmo  28879  tglnpt2  28890  mirreu3  28895  perpcom  28954  colperpexlem3  28974  mideu  28980  opphllem1  28989  hlpasch  28999  lnopp2hpgb  29006  trgcopy  29074  brcgr  29193  brbtwn2  29198  colinearalg  29203  axsegcon  29220  axeuclidlem  29255  axcontlem9  29265  ecgrtg  29276  elntg  29277  eengtrkg  29279  upgr1eopALT  29410  usgredg4  29510  subuhgr  29579  subumgr  29581  usgr2wspthon  30260  clwlkclwwlkf1  30304  eupth2lems  30532  n4cyclfrgr  30585  vacn  30989  blocni  31100  ubthlem3  31167  minvecolem7  31178  chocunii  31596  pjhthmo  31597  pjhthlem2  31687  kbass5  32415  mdsymlem5  32702  foresf1o  32793  fcobij  33008  xrofsup  33055  mgcoval  33249  mgcf1o  33266  xrge0tsmsd  33336  symgcntz  33348  archirngz  33452  archiabllem2a  33457  isarchiofld  33462  mplvrpmmhm  33883  constrelextdg2  34084  smatrcl  34133  reff  34176  ordtconnlem1  34261  qqhval2  34319  volmeas  34568  fiunelcarsg  34653  ballotlemfc0  34830  ballotlemfcc  34831  signstfvneq0  34906  derangenlem  35598  erdsze2lem1  35630  pconnconn  35658  connpconn  35662  cvxsconn  35670  cvmliftmolem2  35709  cvmliftmo  35711  cvmlift2lem10  35739  cvmlift2lem12  35741  cvmlift3lem7  35752  mrsubff1  35941  msubff1  35983  r1peuqusdeg1  36070  ifscgr  36471  cgrxfr  36482  btwnconn1lem13  36526  btwnconn1lem14  36527  outsideofeq  36557  ellines  36579  finminlem  36754  fnejoin2  36805  weiunso  36902  unbdqndv2  37025  irrdiff  37895  qdiff  37896  poimirlem13  38209  poimirlem14  38210  poimirlem32  38228  opnmbllem0  38232  mblfinlem3  38235  itg2addnclem  38247  itg2addnc  38250  ftc1cnnc  38268  upixp  38305  filbcmb  38316  sstotbnd2  38350  isbnd3  38360  prdsbnd2  38371  cntotbnd  38372  ismtyima  38379  bfp  38400  rrncmslem  38408  unichnidl  38607  lshpcmp  39689  islshpat  39718  lfl0f  39770  ishlat3N  40055  3dim1  40168  islvol5  40280  lvoli2  40282  lncvrelatN  40482  pclfinclN  40651  pexmidlem8N  40678  idltrn  40851  cdleme42keg  41187  cdleme42mgN  41189  cdlemf2  41263  cdlemg2cex  41292  trlcoat  41424  dihopelvalcpre  41949  dih1dimatlem  42030  dihjatcclem4  42122  lcfl7N  42202  lcfrlem9  42251  mapdh9a  42490  hdmapglem7  42630  aks4d1p8  42781  isprimroot  42787  evl1gprodd  42811  sticksstones11  42850  grpods  42888  aks5lem8  42895  renegeulemv  43056  sn-subeu  43115  remulinvcom  43121  imacrhmcl  43215  fidomncyc  43232  fsuppind  43251  fsuppssind  43254  mhpind  43255  prjspertr  43266  prjspreln0  43270  flt4lem7  43320  nna4b4nsq  43321  nacsfix  43372  mzpsubst  43408  mzpcompact2lem  43411  eldioph2lem2  43421  eldioph2  43422  eldioph2b  43423  diophin  43432  diophun  43433  irrapxlem3  43480  irrapxlem5  43482  pell1234qrreccl  43510  pell1234qrmulcl  43511  pell14qrdich  43525  pell1qrge1  43526  pell1qrgaplem  43529  monotuz  43597  acongtr  43634  acongrep  43636  jm2.23  43652  jm2.26a  43656  jm2.26lem3  43657  jm2.26  43658  jm2.27  43664  wepwsolem  43698  fnwe2lem2  43707  kelac1  43719  kercvrlsm  43739  hbtlem5  43784  hbt  43786  mpaaeu  43806  cantnfresb  43980  onmcl  43987  tfsconcatun  43993  tfsconcatfn  43994  tfsconcatfv1  43995  tfsconcatfv2  43996  naddcnff  44018  rfovcnvf1od  44659  mnurndlem1  44920  cncmpmax  45681  rfcnnnub  45685  disjxp1  45718  iccintsng  46168  fprodcn  46245  lptioo2  46276  lptioo1  46277  limclner  46294  stoweidlem31  46674  stoweidlem34  46677  stoweidlem35  46678  stoweidlem49  46692  stoweidlem59  46702  stoweidlem62  46705  fourierdlem60  46809  fourierdlem61  46810  fourierdlem87  46836  iundjiun  47103  ismeannd  47110  hoidmvle  47243  smfsuplem2  47455  2reu8i  47776  prproropf1olem2  48179  paireqne  48186  nprmmul2  48203  perfectALTVlem2  48413  mogoldbb  48476  bgoldbtbndlem2  48497  bgoldbtbndlem3  48498  grimedg  48626  grlimprclnbgrvtx  48690  scmsuppss  49073  lindslinindsimp2lem5  49164  elfzolborelfzop1  49221  elbigolo1  49259  itschlc0xyqsol1  49468  itschlc0xyqsol  49469  iccdisj  49598  toslat  49682  iinfssclem3  49756  iinfssc  49757  iinfsubc  49758  imasubc3  49856  upciclem4  49869  uppropd  49881  natoppf  49929  tposcurf1  49999  fuco22  50039  fuco22natlem  50045  functhinclem4  50147  arweuthinc  50229