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 727	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 207  df-an 396

This theorem is referenced by:  disjxiun  5092  frpomin  6292  fsnex  7224  f1prex  7225  isotr  7277  weniso  7295  riota5f  7338  frxp2  8084  frxp3  8091  xpord3pred  8092  poseq  8098  fprlem2  8241  tfrlem9a  8315  oaass  8486  oeeui  8527  oaabs2  8574  coflton  8596  cofon1  8597  naddssim  8610  resixpfo  8870  omxpenlem  9002  pw2f1olem  9005  fopwdom  9009  fofinf1o  9241  marypha1lem  9342  ordiso2  9426  oismo  9451  ixpiunwdom  9501  cantnf  9608  ttrclss  9635  fseqenlem1  9937  iunfictbso  10027  dfac12lem2  10058  dfac12lem3  10059  infunsdom1  10125  infpssrlem5  10220  fin23lem24  10235  isf32lem2  10267  isf32lem4  10269  isf34lem4  10290  fin1a2lem12  10324  fin1a2lem13  10325  ttukeylem6  10427  fpwwe2lem11  10554  fpwwe2lem12  10555  fpwwe2  10556  winalim2  10609  wunex2  10651  tskord  10693  prlem934  10946  mulcmpblnr  10984  dedekind  11297  addrid  11314  cnegex  11315  negeu  11371  add20  11650  divdivdiv  11843  ltmul12a  11998  lemul12a  12000  lediv12a  12036  supaddc  12110  supmul1  12112  cru  12138  uzwo3  12862  xleadd1a  13173  xmullem  13184  xmulgt0  13203  xlemul1a  13208  ixxun  13282  ixxss12  13286  ioodisj  13403  fz0fzelfz0  13555  mulexpz  14027  rpexpmord  14093  leexp1a  14100  expmulnbnd  14160  hashf1  14382  fi1uzind  14432  brfi1indALT  14435  swrdccat  14659  reuccatpfxs1  14671  abs3lem  15264  rexanre  15272  cau3lem  15280  limsupgre  15406  limsupbnd2  15408  o1lo1  15462  rlimclim1  15470  rlimclim  15471  rlimcn1  15513  rlimcn3  15515  o1of2  15538  o1rlimmul  15544  lo1add  15552  lo1mul  15553  isercolllem1  15590  climcau  15596  caucvgrlem  15598  caucvgb  15605  summolem2  15641  summo  15642  modfsummod  15719  o1fsum  15738  prodmolem2  15860  addmodlteqALT  16254  rpdvds  16589  isprm5  16636  isprm6  16643  pclem  16768  pcqmul  16783  pcexp  16789  pcneg  16804  pcprmpw2  16812  pcadd  16819  pcmpt  16822  4sqlem13  16887  vdwlem2  16912  vdwlem7  16917  vdwlem12  16922  ramval  16938  ramub2  16944  ramz2  16954  ramcl  16959  cshwshashlem2  17026  imasval  17433  imasdsval  17437  mreexexd  17572  acsfn  17583  issubc3  17774  idfucl  17806  funcres2c  17828  isnat  17875  fucpropd  17905  xpcval  18101  xpcco  18107  prfval  18123  evlf2  18142  evlfcl  18146  curf12  18151  curf1cl  18152  curf2  18153  curfcl  18156  curf2ndf  18171  hof2val  18180  hofcl  18183  hofpropd  18191  yonedalem4a  18199  yonedainv  18205  drsdirfi  18229  pospo  18267  poslubmo  18333  posglbmo  18334  isipodrs  18461  acsinfd  18480  gsumvalx  18568  gsumpropd2lem  18571  mgmhmeql  18608  sgrppropd  18623  ismndd  18648  mndpropd  18651  mndpsuppss  18657  mhmeql  18718  mndind  18720  frmdup3lem  18758  mhmmnd  18961  issubg4  19042  ssnmz  19063  conjnmzb  19150  f1otrspeq  19344  psgneu  19403  pgpfi  19502  sylow2blem3  19519  slwhash  19521  fislw  19522  sylow3lem2  19525  lsmdisj2  19579  pj1eu  19593  efgredlem  19644  frgpuplem  19669  gexex  19750  frgpnabl  19772  dprdfadd  19919  dpjidcl  19957  pgpfac1lem3  19976  pgpfaclem3  19982  ablfac2  19988  ablsimpgcygd  20005  ablsimpgfind  20009  ablsimpgprmd  20014  rngpropd  20077  ringpropd  20191  imadrhmcl  20700  islmhm2  20960  lmhmpropd  20995  lbsextlem4  21086  prmirredlem  21397  psgndiflemA  21526  lsmcss  21617  uvcf1  21717  frlmsslsp  21721  frlmup1  21723  assapropd  21797  psrval  21840  evlslem1  22005  mamucl  22304  mamuass  22305  mamudi  22306  mamudir  22307  mamuvs1  22308  mamuvs2  22309  mamulid  22344  mamurid  22345  dmatsubcl  22401  dmatmulcl  22403  scmatscm  22416  marrepval  22465  marepveval  22471  mdetunilem7  22521  gsummatr01lem4  22561  cpmatmcllem  22621  mat2pmatf1  22632  mat2pmatlin  22638  decpmatmul  22675  pm2mpmhmlem2  22722  chpidmat  22750  pptbas  22911  toponmre  22996  restbas  23061  iscncl  23172  cnrest2  23189  cnpdis  23196  lmcnp  23207  dishaus  23285  cmpcovf  23294  tgcmp  23304  dfconn2  23322  clsconn  23333  2ndcctbss  23358  dis2ndc  23363  1stccnp  23365  islly2  23387  cldllycmp  23398  locfincmp  23429  comppfsc  23435  kgentopon  23441  txcls  23507  ptpjopn  23515  dfac14  23521  xkoccn  23522  txcnp  23523  txcmpb  23547  txlm  23551  xkopt  23558  xkoco1cn  23560  xkoco2cn  23561  qtopcn  23617  qtoprest  23620  regr1lem2  23643  xkocnv  23717  qtophmeo  23720  fmfnfmlem4  23860  hausflim  23884  hauspwpwf1  23890  fclscmp  23933  alexsublem  23947  alexsubALTlem2  23951  alexsubALTlem3  23952  ptcmplem3  23957  ptcmplem4  23958  ptcmplem5  23959  cnextfun  23967  tmdgsum2  23999  symgtgp  24009  tsmsval2  24033  tsmsgsum  24042  utoptop  24138  ismet2  24237  blin  24325  metss2lem  24415  methaus  24424  met1stc  24425  met2ndci  24426  prdsxmslem2  24433  metcnp3  24444  metcnpi3  24450  metustto  24457  metustfbas  24461  nlmvscn  24591  nrginvrcn  24596  xrsxmet  24714  reconnlem1  24731  reconn  24733  xrge0tsms  24739  xmetdcn2  24742  metdscn  24761  addcnlem  24769  fsumcn  24777  cnheiborlem  24869  cnheibor  24870  bndth  24873  lebnum  24879  nmoleub2lem2  25032  ipcn  25162  iscmet3  25209  caubl  25224  rrxdstprj1  25325  minveclem3b  25344  minveclem7  25351  pjthlem2  25354  pmltpc  25367  volfiniun  25464  ioombl1  25479  dyadss  25511  dyaddisjlem  25512  dyadmax  25515  dyadmbllem  25516  opnmbllem  25518  itg1addlem2  25614  itg10a  25627  mbfi1fseqlem6  25637  itg2seq  25659  itg2monolem1  25667  itg2gt0  25677  itgfsum  25744  limcfval  25789  ellimc2  25794  ellimc3  25796  limcres  25803  limciun  25811  dvres  25828  dveflem  25899  rolle  25910  dvlip2  25916  c1liplem1  25917  dvgt0lem1  25923  dvgt0  25925  dvlt0  25926  dvne0  25932  dvfsumrlimge0  25953  ftc1lem6  25964  itgsubst  25972  mdegmullem  25999  ply1domn  26045  ply1divex  26058  fta1g  26091  fta1b  26093  plyf  26119  dgrlem  26150  coeid  26159  plydivalg  26223  aannenlem1  26252  aalioulem3  26258  aalioulem6  26261  abelthlem8  26365  efif1olem4  26470  chordthm  26763  xrlimcnp  26894  jensen  26915  lgamcvglem  26966  lgamcvg2  26981  sqf11  27065  fsumvma2  27141  perfectlem2  27157  lgsdilem  27251  lgsquad2lem2  27312  lgsquad3  27314  2sqlem5  27349  2sqlem9  27354  2sqb  27359  rpvmasumlem  27414  dchrisum0flb  27437  dchrisum0  27447  pntpbnd  27515  pntibndlem3  27519  pntleml  27538  nolt02o  27623  nosupbday  27633  nosupbnd2  27644  noinfbday  27648  noinfbnd2  27659  noetasuplem4  27664  noetainflem4  27668  noetalem1  27669  conway  27728  slerec  27748  sltlpss  27840  addsprop  27906  bdayon  28196  n0sfincut  28269  eucliddivs  28288  remulscllem2  28388  tgjustc1  28438  tgjustc2  28439  legov  28548  legtrid  28554  tglinethru  28599  tglnpt2  28604  tglineintmo  28605  mirreu3  28617  perpcom  28676  colperpexlem3  28695  mideu  28701  opphllem1  28710  hlpasch  28719  lnopp2hpgb  28726  trgcopy  28767  brcgr  28863  brbtwn2  28868  colinearalg  28873  axsegcon  28890  axeuclidlem  28925  axcontlem9  28935  ecgrtg  28946  elntg  28947  eengtrkg  28949  upgr1eopALT  29080  usgredg4  29180  subuhgr  29249  subumgr  29251  usgr2wspthon  29928  clwlkclwwlkf1  29972  eupth2lems  30200  n4cyclfrgr  30253  vacn  30656  blocni  30767  ubthlem3  30834  minvecolem7  30845  chocunii  31263  pjhthmo  31264  pjhthlem2  31354  kbass5  32082  mdsymlem5  32369  foresf1o  32466  fcobij  32678  xrofsup  32723  mgcoval  32941  mgcf1o  32958  xrge0tsmsd  33028  symgcntz  33040  archirngz  33141  archiabllem2a  33146  isarchiofld  33151  prmidl2  33388  constrelextdg2  33713  smatrcl  33762  reff  33805  ordtconnlem1  33890  qqhval2  33948  volmeas  34197  fiunelcarsg  34283  ballotlemfc0  34460  ballotlemfcc  34461  signstfvneq0  34539  derangenlem  35143  erdsze2lem1  35175  pconnconn  35203  connpconn  35207  cvxsconn  35215  cvmliftmolem2  35254  cvmliftmo  35256  cvmlift2lem10  35284  cvmlift2lem12  35286  cvmlift3lem7  35297  mrsubff1  35486  msubff1  35528  r1peuqusdeg1  35615  ifscgr  36017  cgrxfr  36028  btwnconn1lem13  36072  btwnconn1lem14  36073  outsideofeq  36103  ellines  36125  finminlem  36291  fnejoin2  36342  weiunso  36439  unbdqndv2  36484  irrdiff  37299  poimirlem13  37612  poimirlem14  37613  poimirlem32  37631  opnmbllem0  37635  mblfinlem3  37638  itg2addnclem  37650  itg2addnc  37653  ftc1cnnc  37671  upixp  37708  filbcmb  37719  sstotbnd2  37753  isbnd3  37763  prdsbnd2  37774  cntotbnd  37775  ismtyima  37782  bfp  37803  rrncmslem  37811  unichnidl  38010  lshpcmp  38966  islshpat  38995  lfl0f  39047  ishlat3N  39332  3dim1  39446  islvol5  39558  lvoli2  39560  lncvrelatN  39760  pclfinclN  39929  pexmidlem8N  39956  idltrn  40129  cdleme42keg  40465  cdleme42mgN  40467  cdlemf2  40541  cdlemg2cex  40570  trlcoat  40702  dihopelvalcpre  41227  dih1dimatlem  41308  dihjatcclem4  41400  lcfl7N  41480  lcfrlem9  41529  mapdh9a  41768  hdmapglem7  41908  aks4d1p8  42060  isprimroot  42066  evl1gprodd  42090  sticksstones11  42129  grpods  42167  aks5lem8  42174  renegeulemv  42341  sn-subeu  42400  remulinvcom  42406  imacrhmcl  42487  fidomncyc  42508  fsuppind  42563  fsuppssind  42566  mhpind  42567  prjspertr  42578  prjspreln0  42582  flt4lem7  42632  nna4b4nsq  42633  nacsfix  42685  mzpsubst  42721  mzpcompact2lem  42724  eldioph2lem2  42734  eldioph2  42735  eldioph2b  42736  diophin  42745  diophun  42746  irrapxlem3  42797  irrapxlem5  42799  pell1234qrreccl  42827  pell1234qrmulcl  42828  pell14qrdich  42842  pell1qrge1  42843  pell1qrgaplem  42846  monotuz  42914  acongtr  42951  acongrep  42953  jm2.23  42969  jm2.26a  42973  jm2.26lem3  42974  jm2.26  42975  jm2.27  42981  wepwsolem  43015  fnwe2lem2  43024  kelac1  43036  kercvrlsm  43056  hbtlem5  43101  hbt  43103  mpaaeu  43123  cantnfresb  43297  onmcl  43304  tfsconcatun  43310  tfsconcatfn  43311  tfsconcatfv1  43312  tfsconcatfv2  43313  naddcnff  43335  rfovcnvf1od  43977  mnurndlem1  44254  cncmpmax  45010  rfcnnnub  45014  disjxp1  45047  iccintsng  45505  fprodcn  45582  lptioo2  45613  lptioo1  45614  limclner  45633  stoweidlem31  46013  stoweidlem34  46016  stoweidlem35  46017  stoweidlem49  46031  stoweidlem59  46041  stoweidlem62  46044  fourierdlem60  46148  fourierdlem61  46149  fourierdlem87  46175  iundjiun  46442  ismeannd  46449  hoidmvle  46582  smfsuplem2  46794  2reu8i  47098  prproropf1olem2  47489  paireqne  47496  perfectALTVlem2  47707  mogoldbb  47770  bgoldbtbndlem2  47791  bgoldbtbndlem3  47792  grimedg  47919  scmsuppss  48343  lindslinindsimp2lem5  48435  elfzolborelfzop1  48492  elbigolo1  48530  itschlc0xyqsol1  48739  itschlc0xyqsol  48740  iccdisj  48870  toslat  48954  iinfssclem3  49029  iinfssc  49030  iinfsubc  49031  imasubc3  49129  upciclem4  49142  uppropd  49154  natoppf  49202  tposcurf1  49272  fuco22  49312  fuco22natlem  49318  functhinclem4  49420  arweuthinc  49502