Theorem simplrr 774

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  disjxiun  4965  fsnex  6911  f1prex  6912  isotr  6959  weniso  6977  riota5f  7009  tfrlem9a  7881  oaass  8044  oeeui  8085  oaabs2  8129  resixpfo  8355  omxpenlem  8472  pw2f1olem  8475  fopwdom  8479  fofinf1o  8652  marypha1lem  8750  ordiso2  8832  oismo  8857  ixpiunwdom  8908  cantnf  9009  fseqenlem1  9303  iunfictbso  9393  dfac12lem2  9423  dfac12lem3  9424  infunsdom1  9488  infpssrlem5  9582  fin23lem24  9597  isf32lem2  9629  isf32lem4  9631  isf34lem4  9652  fin1a2lem12  9686  fin1a2lem13  9687  ttukeylem6  9789  fpwwe2lem12  9916  fpwwe2lem13  9917  fpwwe2  9918  winalim2  9971  wunex2  10013  tskord  10055  prlem934  10308  mulcmpblnr  10346  dedekind  10656  addid1  10673  cnegex  10674  negeu  10729  add20  11006  divdivdiv  11195  ltmul12a  11350  lemul12a  11352  lediv12a  11387  supaddc  11462  supmul1  11464  cru  11484  uzwo3  12196  xleadd1a  12500  xmullem  12511  xmulgt0  12530  xlemul1a  12535  ixxun  12608  ixxss12  12612  ioodisj  12722  fz0fzelfz0  12867  mulexpz  13323  rpexpmord  13386  leexp1a  13393  expmulnbnd  13450  hashf1  13667  fi1uzind  13705  brfi1indALT  13708  swrdccat  13937  reuccatpfxs1  13949  abs3lem  14536  rexanre  14544  cau3lem  14552  limsupgre  14676  limsupbnd2  14678  o1lo1  14732  rlimclim1  14740  rlimclim  14741  rlimcn1  14783  rlimcn2  14785  o1of2  14807  o1rlimmul  14813  lo1add  14821  lo1mul  14822  isercolllem1  14859  climcau  14865  caucvgrlem  14867  caucvgb  14874  summolem2  14910  summo  14911  modfsummod  14986  o1fsum  15005  prodmolem2  15126  addmodlteqALT  15512  rpdvds  15837  isprm5  15884  isprm6  15891  pclem  16008  pcqmul  16023  pcexp  16029  pcneg  16043  pcprmpw2  16051  pcadd  16058  pcmpt  16061  4sqlem13  16126  vdwlem2  16151  vdwlem7  16156  vdwlem12  16161  ramval  16177  ramub2  16183  ramz2  16193  ramcl  16198  cshwshashlem2  16263  imasval  16617  imasdsval  16621  mreexexd  16752  acsfn  16763  issubc3  16952  idfucl  16984  funcres2c  17004  isnat  17050  fucpropd  17080  xpcval  17260  xpcco  17266  prfval  17282  evlf2  17301  evlfcl  17305  curf12  17310  curf1cl  17311  curf2  17312  curfcl  17315  curf2ndf  17330  hof2val  17339  hofcl  17342  hofpropd  17350  yonedalem4a  17358  yonedainv  17364  drsdirfi  17381  pospo  17416  poslubmo  17589  posglbmo  17590  isipodrs  17604  acsinfd  17623  gsumvalx  17713  gsumpropd2lem  17716  ismndd  17756  mndpropd  17759  mhmeql  17807  mndind  17809  frmdup3lem  17846  mhmmnd  17982  issubg4  18056  ssnmz  18079  conjnmzb  18138  f1otrspeq  18310  psgneu  18369  pgpfi  18464  sylow2blem3  18481  slwhash  18483  fislw  18484  sylow3lem2  18487  lsmdisj2  18539  pj1eu  18553  efgredlem  18604  frgpuplem  18629  gexex  18700  frgpnabl  18722  dprdfadd  18863  dpjidcl  18901  pgpfac1lem3  18920  pgpfaclem3  18926  ablfac2  18932  ringpropd  19026  islmhm2  19504  lmhmpropd  19539  lbsextlem4  19627  assapropd  19793  psrval  19834  evlslem1  19986  prmirredlem  20326  psgndiflemA  20431  lsmcss  20522  uvcf1  20622  frlmsslsp  20626  frlmup1  20628  mamucl  20698  mamuass  20699  mamudi  20700  mamudir  20701  mamuvs1  20702  mamuvs2  20703  mamulid  20738  mamurid  20739  dmatsubcl  20795  dmatmulcl  20797  scmatscm  20810  marrepval  20859  marepveval  20865  mdetunilem7  20915  gsummatr01lem4  20955  cpmatmcllem  21014  mat2pmatf1  21025  mat2pmatlin  21031  decpmatmul  21068  pm2mpmhmlem2  21115  chpidmat  21143  pptbas  21304  toponmre  21389  restbas  21454  iscncl  21565  cnrest2  21582  cnpdis  21589  lmcnp  21600  dishaus  21678  cmpcovf  21687  tgcmp  21697  dfconn2  21715  clsconn  21726  2ndcctbss  21751  dis2ndc  21756  1stccnp  21758  islly2  21780  cldllycmp  21791  locfincmp  21822  comppfsc  21828  kgentopon  21834  txcls  21900  ptpjopn  21908  dfac14  21914  xkoccn  21915  txcnp  21916  txcmpb  21940  txlm  21944  xkopt  21951  xkoco1cn  21953  xkoco2cn  21954  qtopcn  22010  qtoprest  22013  regr1lem2  22036  xkocnv  22110  qtophmeo  22113  fmfnfmlem4  22253  hausflim  22277  hauspwpwf1  22283  fclscmp  22326  alexsublem  22340  alexsubALTlem2  22344  alexsubALTlem3  22345  ptcmplem3  22350  ptcmplem4  22351  ptcmplem5  22352  cnextfun  22360  tmdgsum2  22392  symgtgp  22397  tsmsval2  22425  tsmsgsum  22434  utoptop  22530  ismet2  22630  blin  22718  metss2lem  22808  methaus  22817  met1stc  22818  met2ndci  22819  prdsxmslem2  22826  metcnp3  22837  metcnpi3  22843  metustto  22850  metustfbas  22854  nlmvscn  22983  nrginvrcn  22988  xrsxmet  23104  reconnlem1  23121  reconn  23123  xrge0tsms  23129  xmetdcn2  23132  metdscn  23151  addcnlem  23159  fsumcn  23165  cnheiborlem  23245  cnheibor  23246  bndth  23249  lebnum  23255  nmoleub2lem2  23407  ipcn  23536  iscmet3  23583  caubl  23598  rrxdstprj1  23699  minveclem3b  23718  minveclem7  23725  pjthlem2  23728  pmltpc  23738  volfiniun  23835  ioombl1  23850  dyadss  23882  dyaddisjlem  23883  dyadmax  23886  dyadmbllem  23887  opnmbllem  23889  itg1addlem2  23985  itg10a  23998  mbfi1fseqlem6  24008  itg2seq  24030  itg2monolem1  24038  itg2gt0  24048  itgfsum  24114  limcfval  24157  ellimc2  24162  ellimc3  24164  limcres  24171  limciun  24179  dvres  24196  dveflem  24263  rolle  24274  dvlip2  24279  c1liplem1  24280  dvgt0lem1  24286  dvgt0  24288  dvlt0  24289  dvne0  24295  dvfsumrlimge0  24314  ftc1lem6  24325  itgsubst  24333  mdegmullem  24359  ply1domn  24404  ply1divex  24417  fta1g  24448  fta1b  24450  plyf  24475  dgrlem  24506  coeid  24515  plydivalg  24575  aannenlem1  24604  aalioulem3  24610  aalioulem6  24613  abelthlem8  24714  efif1olem4  24814  chordthm  25100  xrlimcnp  25232  jensen  25252  lgamcvglem  25303  lgamcvg2  25318  sqf11  25402  fsumvma2  25476  perfectlem2  25492  lgsdilem  25586  lgsquad2lem2  25647  lgsquad3  25649  2sqlem5  25684  2sqlem9  25689  2sqb  25694  rpvmasumlem  25749  dchrisum0flb  25772  dchrisum0  25782  pntpbnd  25850  pntibndlem3  25854  pntleml  25873  tgjustc1  25947  tgjustc2  25948  legov  26057  legtrid  26063  tglinethru  26108  tglnpt2  26113  tglineintmo  26114  mirreu3  26126  perpcom  26185  colperpexlem3  26204  mideu  26210  opphllem1  26219  hlpasch  26228  lnopp2hpgb  26235  trgcopy  26276  brcgr  26373  brbtwn2  26378  colinearalg  26383  axsegcon  26400  axeuclidlem  26435  axcontlem9  26445  ecgrtg  26456  elntg  26457  eengtrkg  26459  upgr1eopALT  26589  usgredg4  26686  subuhgr  26755  subumgr  26757  usgr2wspthon  27430  clwlkclwwlkf1  27474  eupth2lems  27703  n4cyclfrgr  27758  vacn  28158  blocni  28269  ubthlem3  28336  minvecolem7  28347  chocunii  28765  pjhthmo  28766  pjhthlem2  28856  kbass5  29584  mdsymlem5  29871  foresf1o  29953  fcobij  30142  xrofsup  30176  symgcntz  30384  archirngz  30452  archiabllem2a  30457  xrge0tsmsd  30499  isarchiofld  30540  smatrcl  30672  reff  30716  ordtconnlem1  30780  qqhval2  30836  volmeas  31103  fiunelcarsg  31187  ballotlemfc0  31363  ballotlemfcc  31364  signstfvneq0  31455  derangenlem  32028  erdsze2lem1  32060  pconnconn  32088  connpconn  32092  cvxsconn  32100  cvmliftmolem2  32139  cvmliftmo  32141  cvmlift2lem10  32169  cvmlift2lem12  32171  cvmlift3lem7  32182  mrsubff1  32371  msubff1  32413  frpomin  32689  poseq  32706  fprlem2  32749  nolt02o  32810  noprefixmo  32813  nosupbnd2  32827  noetalem3  32830  noetalem5  32832  conway  32875  slerec  32888  ifscgr  33116  cgrxfr  33127  btwnconn1lem13  33171  btwnconn1lem14  33172  outsideofeq  33202  ellines  33224  finminlem  33277  fnejoin2  33328  unbdqndv2  33461  poimirlem13  34457  poimirlem14  34458  poimirlem32  34476  opnmbllem0  34480  mblfinlem3  34483  itg2addnclem  34495  itg2addnc  34498  ftc1cnnc  34518  upixp  34557  filbcmb  34568  sstotbnd2  34605  isbnd3  34615  prdsbnd2  34626  cntotbnd  34627  ismtyima  34634  bfp  34655  rrncmslem  34663  unichnidl  34862  lshpcmp  35676  islshpat  35705  lfl0f  35757  ishlat3N  36042  3dim1  36155  islvol5  36267  lvoli2  36269  lncvrelatN  36469  pclfinclN  36638  pexmidlem8N  36665  idltrn  36838  cdleme42keg  37174  cdleme42mgN  37176  cdlemf2  37250  cdlemg2cex  37279  trlcoat  37411  dihopelvalcpre  37936  dih1dimatlem  38017  dihjatcclem4  38109  lcfl7N  38189  lcfrlem9  38238  mapdh9a  38477  hdmapglem7  38617  renegeulemv  38741  prjspertr  38773  prjspreln0  38777  nacsfix  38815  mzpsubst  38851  mzpcompact2lem  38854  eldioph2lem2  38864  eldioph2  38865  eldioph2b  38866  diophin  38875  diophun  38876  irrapxlem3  38927  irrapxlem5  38929  pell1234qrreccl  38957  pell1234qrmulcl  38958  pell14qrdich  38972  pell1qrge1  38973  pell1qrgaplem  38976  monotuz  39044  acongtr  39081  acongrep  39083  jm2.23  39099  jm2.26a  39103  jm2.26lem3  39104  jm2.26  39105  jm2.27  39111  wepwsolem  39148  fnwe2lem2  39157  kelac1  39169  kercvrlsm  39189  hbtlem5  39234  hbt  39236  mpaaeu  39256  rfovcnvf1od  39856  mnurndlem1  40135  ablsimpgcygd  40185  ablsimpgfind  40188  ablsimpgprmd  40193  cncmpmax  40849  rfcnnnub  40853  disjxp1  40891  iccintsng  41362  fprodcn  41444  lptioo2  41475  lptioo1  41476  limclner  41495  stoweidlem31  41880  stoweidlem34  41883  stoweidlem35  41884  stoweidlem49  41898  stoweidlem59  41908  stoweidlem62  41911  fourierdlem60  42015  fourierdlem61  42016  fourierdlem87  42042  iundjiun  42306  ismeannd  42313  hoidmvle  42446  smfsuplem2  42650  2reu8i  42850  prproropf1olem2  43170  paireqne  43177  perfectALTVlem2  43391  mogoldbb  43454  bgoldbtbndlem2  43475  bgoldbtbndlem3  43476  isomgrtrlem  43507  mgmhmeql  43574  mndpsuppss  43921  scmsuppss  43922  lindslinindsimp2lem5  44019  elfzolborelfzop1  44077  elbigolo1  44120  itschlc0xyqsol1  44256  itschlc0xyqsol  44257