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 726	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  5163  frpomin  6372  fsnex  7319  f1prex  7320  isotr  7372  weniso  7390  riota5f  7433  frxp2  8185  frxp3  8192  xpord3pred  8193  poseq  8199  fprlem2  8342  tfrlem9a  8442  oaass  8617  oeeui  8658  oaabs2  8705  coflton  8727  cofon1  8728  naddssim  8741  resixpfo  8994  omxpenlem  9139  pw2f1olem  9142  fopwdom  9146  fofinf1o  9400  marypha1lem  9502  ordiso2  9584  oismo  9609  ixpiunwdom  9659  cantnf  9762  ttrclss  9789  fseqenlem1  10093  iunfictbso  10183  dfac12lem2  10214  dfac12lem3  10215  infunsdom1  10281  infpssrlem5  10376  fin23lem24  10391  isf32lem2  10423  isf32lem4  10425  isf34lem4  10446  fin1a2lem12  10480  fin1a2lem13  10481  ttukeylem6  10583  fpwwe2lem11  10710  fpwwe2lem12  10711  fpwwe2  10712  winalim2  10765  wunex2  10807  tskord  10849  prlem934  11102  mulcmpblnr  11140  dedekind  11453  addrid  11470  cnegex  11471  negeu  11526  add20  11802  divdivdiv  11995  ltmul12a  12150  lemul12a  12152  lediv12a  12188  supaddc  12262  supmul1  12264  cru  12285  uzwo3  13008  xleadd1a  13315  xmullem  13326  xmulgt0  13345  xlemul1a  13350  ixxun  13423  ixxss12  13427  ioodisj  13542  fz0fzelfz0  13691  mulexpz  14153  rpexpmord  14218  leexp1a  14225  expmulnbnd  14284  hashf1  14506  fi1uzind  14556  brfi1indALT  14559  swrdccat  14783  reuccatpfxs1  14795  abs3lem  15387  rexanre  15395  cau3lem  15403  limsupgre  15527  limsupbnd2  15529  o1lo1  15583  rlimclim1  15591  rlimclim  15592  rlimcn1  15634  rlimcn3  15636  o1of2  15659  o1rlimmul  15665  lo1add  15673  lo1mul  15674  isercolllem1  15713  climcau  15719  caucvgrlem  15721  caucvgb  15728  summolem2  15764  summo  15765  modfsummod  15842  o1fsum  15861  prodmolem2  15983  addmodlteqALT  16373  rpdvds  16707  isprm5  16754  isprm6  16761  pclem  16885  pcqmul  16900  pcexp  16906  pcneg  16921  pcprmpw2  16929  pcadd  16936  pcmpt  16939  4sqlem13  17004  vdwlem2  17029  vdwlem7  17034  vdwlem12  17039  ramval  17055  ramub2  17061  ramz2  17071  ramcl  17076  cshwshashlem2  17144  imasval  17571  imasdsval  17575  mreexexd  17706  acsfn  17717  issubc3  17913  idfucl  17945  funcres2c  17968  isnat  18015  fucpropd  18047  xpcval  18246  xpcco  18252  prfval  18268  evlf2  18288  evlfcl  18292  curf12  18297  curf1cl  18298  curf2  18299  curfcl  18302  curf2ndf  18317  hof2val  18326  hofcl  18329  hofpropd  18337  yonedalem4a  18345  yonedainv  18351  drsdirfi  18375  pospo  18415  poslubmo  18481  posglbmo  18482  isipodrs  18607  acsinfd  18626  gsumvalx  18714  gsumpropd2lem  18717  mgmhmeql  18754  sgrppropd  18769  ismndd  18794  mndpropd  18797  mhmeql  18861  mndind  18863  frmdup3lem  18901  mhmmnd  19104  issubg4  19185  ssnmz  19206  conjnmzb  19293  f1otrspeq  19489  psgneu  19548  pgpfi  19647  sylow2blem3  19664  slwhash  19666  fislw  19667  sylow3lem2  19670  lsmdisj2  19724  pj1eu  19738  efgredlem  19789  frgpuplem  19814  gexex  19895  frgpnabl  19917  dprdfadd  20064  dpjidcl  20102  pgpfac1lem3  20121  pgpfaclem3  20127  ablfac2  20133  ablsimpgcygd  20150  ablsimpgfind  20154  ablsimpgprmd  20159  rngpropd  20201  ringpropd  20311  imadrhmcl  20820  islmhm2  21060  lmhmpropd  21095  lbsextlem4  21186  prmirredlem  21506  psgndiflemA  21642  lsmcss  21733  uvcf1  21835  frlmsslsp  21839  frlmup1  21841  assapropd  21915  psrval  21958  evlslem1  22129  mamucl  22426  mamuass  22427  mamudi  22428  mamudir  22429  mamuvs1  22430  mamuvs2  22431  mamulid  22468  mamurid  22469  dmatsubcl  22525  dmatmulcl  22527  scmatscm  22540  marrepval  22589  marepveval  22595  mdetunilem7  22645  gsummatr01lem4  22685  cpmatmcllem  22745  mat2pmatf1  22756  mat2pmatlin  22762  decpmatmul  22799  pm2mpmhmlem2  22846  chpidmat  22874  pptbas  23036  toponmre  23122  restbas  23187  iscncl  23298  cnrest2  23315  cnpdis  23322  lmcnp  23333  dishaus  23411  cmpcovf  23420  tgcmp  23430  dfconn2  23448  clsconn  23459  2ndcctbss  23484  dis2ndc  23489  1stccnp  23491  islly2  23513  cldllycmp  23524  locfincmp  23555  comppfsc  23561  kgentopon  23567  txcls  23633  ptpjopn  23641  dfac14  23647  xkoccn  23648  txcnp  23649  txcmpb  23673  txlm  23677  xkopt  23684  xkoco1cn  23686  xkoco2cn  23687  qtopcn  23743  qtoprest  23746  regr1lem2  23769  xkocnv  23843  qtophmeo  23846  fmfnfmlem4  23986  hausflim  24010  hauspwpwf1  24016  fclscmp  24059  alexsublem  24073  alexsubALTlem2  24077  alexsubALTlem3  24078  ptcmplem3  24083  ptcmplem4  24084  ptcmplem5  24085  cnextfun  24093  tmdgsum2  24125  symgtgp  24135  tsmsval2  24159  tsmsgsum  24168  utoptop  24264  ismet2  24364  blin  24452  metss2lem  24545  methaus  24554  met1stc  24555  met2ndci  24556  prdsxmslem2  24563  metcnp3  24574  metcnpi3  24580  metustto  24587  metustfbas  24591  nlmvscn  24729  nrginvrcn  24734  xrsxmet  24850  reconnlem1  24867  reconn  24869  xrge0tsms  24875  xmetdcn2  24878  metdscn  24897  addcnlem  24905  fsumcn  24913  cnheiborlem  25005  cnheibor  25006  bndth  25009  lebnum  25015  nmoleub2lem2  25168  ipcn  25299  iscmet3  25346  caubl  25361  rrxdstprj1  25462  minveclem3b  25481  minveclem7  25488  pjthlem2  25491  pmltpc  25504  volfiniun  25601  ioombl1  25616  dyadss  25648  dyaddisjlem  25649  dyadmax  25652  dyadmbllem  25653  opnmbllem  25655  itg1addlem2  25751  itg10a  25765  mbfi1fseqlem6  25775  itg2seq  25797  itg2monolem1  25805  itg2gt0  25815  itgfsum  25882  limcfval  25927  ellimc2  25932  ellimc3  25934  limcres  25941  limciun  25949  dvres  25966  dveflem  26037  rolle  26048  dvlip2  26054  c1liplem1  26055  dvgt0lem1  26061  dvgt0  26063  dvlt0  26064  dvne0  26070  dvfsumrlimge0  26091  ftc1lem6  26102  itgsubst  26110  mdegmullem  26137  ply1domn  26183  ply1divex  26196  fta1g  26229  fta1b  26231  plyf  26257  dgrlem  26288  coeid  26297  plydivalg  26359  aannenlem1  26388  aalioulem3  26394  aalioulem6  26397  abelthlem8  26501  efif1olem4  26605  chordthm  26898  xrlimcnp  27029  jensen  27050  lgamcvglem  27101  lgamcvg2  27116  sqf11  27200  fsumvma2  27276  perfectlem2  27292  lgsdilem  27386  lgsquad2lem2  27447  lgsquad3  27449  2sqlem5  27484  2sqlem9  27489  2sqb  27494  rpvmasumlem  27549  dchrisum0flb  27572  dchrisum0  27582  pntpbnd  27650  pntibndlem3  27654  pntleml  27673  nolt02o  27758  nosupbday  27768  nosupbnd2  27779  noinfbday  27783  noinfbnd2  27794  noetasuplem4  27799  noetainflem4  27803  noetalem1  27804  conway  27862  slerec  27882  sltlpss  27963  addsprop  28027  remulscllem2  28451  tgjustc1  28501  tgjustc2  28502  legov  28611  legtrid  28617  tglinethru  28662  tglnpt2  28667  tglineintmo  28668  mirreu3  28680  perpcom  28739  colperpexlem3  28758  mideu  28764  opphllem1  28773  hlpasch  28782  lnopp2hpgb  28789  trgcopy  28830  brcgr  28933  brbtwn2  28938  colinearalg  28943  axsegcon  28960  axeuclidlem  28995  axcontlem9  29005  ecgrtg  29016  elntg  29017  eengtrkg  29019  upgr1eopALT  29152  usgredg4  29252  subuhgr  29321  subumgr  29323  usgr2wspthon  29998  clwlkclwwlkf1  30042  eupth2lems  30270  n4cyclfrgr  30323  vacn  30726  blocni  30837  ubthlem3  30904  minvecolem7  30915  chocunii  31333  pjhthmo  31334  pjhthlem2  31424  kbass5  32152  mdsymlem5  32439  foresf1o  32532  fcobij  32736  xrofsup  32774  mgcoval  32959  mgcf1o  32976  xrge0tsmsd  33041  symgcntz  33078  archirngz  33169  archiabllem2a  33174  isarchiofld  33312  prmidl2  33434  constrelextdg2  33737  smatrcl  33742  reff  33785  ordtconnlem1  33870  qqhval2  33928  volmeas  34195  fiunelcarsg  34281  ballotlemfc0  34457  ballotlemfcc  34458  signstfvneq0  34549  derangenlem  35139  erdsze2lem1  35171  pconnconn  35199  connpconn  35203  cvxsconn  35211  cvmliftmolem2  35250  cvmliftmo  35252  cvmlift2lem10  35280  cvmlift2lem12  35282  cvmlift3lem7  35293  mrsubff1  35482  msubff1  35524  r1peuqusdeg1  35611  ifscgr  36008  cgrxfr  36019  btwnconn1lem13  36063  btwnconn1lem14  36064  outsideofeq  36094  ellines  36116  finminlem  36284  fnejoin2  36335  weiunso  36432  unbdqndv2  36477  irrdiff  37292  poimirlem13  37593  poimirlem14  37594  poimirlem32  37612  opnmbllem0  37616  mblfinlem3  37619  itg2addnclem  37631  itg2addnc  37634  ftc1cnnc  37652  upixp  37689  filbcmb  37700  sstotbnd2  37734  isbnd3  37744  prdsbnd2  37755  cntotbnd  37756  ismtyima  37763  bfp  37784  rrncmslem  37792  unichnidl  37991  lshpcmp  38944  islshpat  38973  lfl0f  39025  ishlat3N  39310  3dim1  39424  islvol5  39536  lvoli2  39538  lncvrelatN  39738  pclfinclN  39907  pexmidlem8N  39934  idltrn  40107  cdleme42keg  40443  cdleme42mgN  40445  cdlemf2  40519  cdlemg2cex  40548  trlcoat  40680  dihopelvalcpre  41205  dih1dimatlem  41286  dihjatcclem4  41378  lcfl7N  41458  lcfrlem9  41507  mapdh9a  41746  hdmapglem7  41886  aks4d1p8  42044  isprimroot  42050  evl1gprodd  42074  sticksstones11  42113  grpods  42151  aks5lem8  42158  renegeulemv  42344  sn-subeu  42402  remulinvcom  42408  sn-itrere  42444  sn-retire  42445  imacrhmcl  42469  fidomncyc  42490  fsuppind  42545  fsuppssind  42548  mhpind  42549  prjspertr  42560  prjspreln0  42564  flt4lem7  42614  nna4b4nsq  42615  nacsfix  42668  mzpsubst  42704  mzpcompact2lem  42707  eldioph2lem2  42717  eldioph2  42718  eldioph2b  42719  diophin  42728  diophun  42729  irrapxlem3  42780  irrapxlem5  42782  pell1234qrreccl  42810  pell1234qrmulcl  42811  pell14qrdich  42825  pell1qrge1  42826  pell1qrgaplem  42829  monotuz  42898  acongtr  42935  acongrep  42937  jm2.23  42953  jm2.26a  42957  jm2.26lem3  42958  jm2.26  42959  jm2.27  42965  wepwsolem  42999  fnwe2lem2  43008  kelac1  43020  kercvrlsm  43040  hbtlem5  43085  hbt  43087  mpaaeu  43107  cantnfresb  43286  onmcl  43293  tfsconcatun  43299  tfsconcatfn  43300  tfsconcatfv1  43301  tfsconcatfv2  43302  naddcnff  43324  rfovcnvf1od  43966  mnurndlem1  44250  cncmpmax  44932  rfcnnnub  44936  disjxp1  44971  iccintsng  45441  fprodcn  45521  lptioo2  45552  lptioo1  45553  limclner  45572  stoweidlem31  45952  stoweidlem34  45955  stoweidlem35  45956  stoweidlem49  45970  stoweidlem59  45980  stoweidlem62  45983  fourierdlem60  46087  fourierdlem61  46088  fourierdlem87  46114  iundjiun  46381  ismeannd  46388  hoidmvle  46521  smfsuplem2  46733  2reu8i  47028  prproropf1olem2  47378  paireqne  47385  perfectALTVlem2  47596  mogoldbb  47659  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  uspgrimprop  47757  grimedg  47787  mndpsuppss  48096  scmsuppss  48097  lindslinindsimp2lem5  48191  elfzolborelfzop1  48248  elbigolo1  48291  itschlc0xyqsol1  48500  itschlc0xyqsol  48501  iccdisj  48578  toslat  48654  functhinclem4  48711