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  5107  frpomin  6316  fsnex  7261  f1prex  7262  isotr  7314  weniso  7332  riota5f  7375  frxp2  8126  frxp3  8133  xpord3pred  8134  poseq  8140  fprlem2  8283  tfrlem9a  8357  oaass  8528  oeeui  8569  oaabs2  8616  coflton  8638  cofon1  8639  naddssim  8652  resixpfo  8912  omxpenlem  9047  pw2f1olem  9050  fopwdom  9054  fofinf1o  9290  marypha1lem  9391  ordiso2  9475  oismo  9500  ixpiunwdom  9550  cantnf  9653  ttrclss  9680  fseqenlem1  9984  iunfictbso  10074  dfac12lem2  10105  dfac12lem3  10106  infunsdom1  10172  infpssrlem5  10267  fin23lem24  10282  isf32lem2  10314  isf32lem4  10316  isf34lem4  10337  fin1a2lem12  10371  fin1a2lem13  10372  ttukeylem6  10474  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  winalim2  10656  wunex2  10698  tskord  10740  prlem934  10993  mulcmpblnr  11031  dedekind  11344  addrid  11361  cnegex  11362  negeu  11418  add20  11697  divdivdiv  11890  ltmul12a  12045  lemul12a  12047  lediv12a  12083  supaddc  12157  supmul1  12159  cru  12185  uzwo3  12909  xleadd1a  13220  xmullem  13231  xmulgt0  13250  xlemul1a  13255  ixxun  13329  ixxss12  13333  ioodisj  13450  fz0fzelfz0  13602  mulexpz  14074  rpexpmord  14140  leexp1a  14147  expmulnbnd  14207  hashf1  14429  fi1uzind  14479  brfi1indALT  14482  swrdccat  14707  reuccatpfxs1  14719  abs3lem  15312  rexanre  15320  cau3lem  15328  limsupgre  15454  limsupbnd2  15456  o1lo1  15510  rlimclim1  15518  rlimclim  15519  rlimcn1  15561  rlimcn3  15563  o1of2  15586  o1rlimmul  15592  lo1add  15600  lo1mul  15601  isercolllem1  15638  climcau  15644  caucvgrlem  15646  caucvgb  15653  summolem2  15689  summo  15690  modfsummod  15767  o1fsum  15786  prodmolem2  15908  addmodlteqALT  16302  rpdvds  16637  isprm5  16684  isprm6  16691  pclem  16816  pcqmul  16831  pcexp  16837  pcneg  16852  pcprmpw2  16860  pcadd  16867  pcmpt  16870  4sqlem13  16935  vdwlem2  16960  vdwlem7  16965  vdwlem12  16970  ramval  16986  ramub2  16992  ramz2  17002  ramcl  17007  cshwshashlem2  17074  imasval  17481  imasdsval  17485  mreexexd  17616  acsfn  17627  issubc3  17818  idfucl  17850  funcres2c  17872  isnat  17919  fucpropd  17949  xpcval  18145  xpcco  18151  prfval  18167  evlf2  18186  evlfcl  18190  curf12  18195  curf1cl  18196  curf2  18197  curfcl  18200  curf2ndf  18215  hof2val  18224  hofcl  18227  hofpropd  18235  yonedalem4a  18243  yonedainv  18249  drsdirfi  18273  pospo  18311  poslubmo  18377  posglbmo  18378  isipodrs  18503  acsinfd  18522  gsumvalx  18610  gsumpropd2lem  18613  mgmhmeql  18650  sgrppropd  18665  ismndd  18690  mndpropd  18693  mndpsuppss  18699  mhmeql  18760  mndind  18762  frmdup3lem  18800  mhmmnd  19003  issubg4  19084  ssnmz  19105  conjnmzb  19192  f1otrspeq  19384  psgneu  19443  pgpfi  19542  sylow2blem3  19559  slwhash  19561  fislw  19562  sylow3lem2  19565  lsmdisj2  19619  pj1eu  19633  efgredlem  19684  frgpuplem  19709  gexex  19790  frgpnabl  19812  dprdfadd  19959  dpjidcl  19997  pgpfac1lem3  20016  pgpfaclem3  20022  ablfac2  20028  ablsimpgcygd  20045  ablsimpgfind  20049  ablsimpgprmd  20054  rngpropd  20090  ringpropd  20204  imadrhmcl  20713  islmhm2  20952  lmhmpropd  20987  lbsextlem4  21078  prmirredlem  21389  psgndiflemA  21517  lsmcss  21608  uvcf1  21708  frlmsslsp  21712  frlmup1  21714  assapropd  21788  psrval  21831  evlslem1  21996  mamucl  22295  mamuass  22296  mamudi  22297  mamudir  22298  mamuvs1  22299  mamuvs2  22300  mamulid  22335  mamurid  22336  dmatsubcl  22392  dmatmulcl  22394  scmatscm  22407  marrepval  22456  marepveval  22462  mdetunilem7  22512  gsummatr01lem4  22552  cpmatmcllem  22612  mat2pmatf1  22623  mat2pmatlin  22629  decpmatmul  22666  pm2mpmhmlem2  22713  chpidmat  22741  pptbas  22902  toponmre  22987  restbas  23052  iscncl  23163  cnrest2  23180  cnpdis  23187  lmcnp  23198  dishaus  23276  cmpcovf  23285  tgcmp  23295  dfconn2  23313  clsconn  23324  2ndcctbss  23349  dis2ndc  23354  1stccnp  23356  islly2  23378  cldllycmp  23389  locfincmp  23420  comppfsc  23426  kgentopon  23432  txcls  23498  ptpjopn  23506  dfac14  23512  xkoccn  23513  txcnp  23514  txcmpb  23538  txlm  23542  xkopt  23549  xkoco1cn  23551  xkoco2cn  23552  qtopcn  23608  qtoprest  23611  regr1lem2  23634  xkocnv  23708  qtophmeo  23711  fmfnfmlem4  23851  hausflim  23875  hauspwpwf1  23881  fclscmp  23924  alexsublem  23938  alexsubALTlem2  23942  alexsubALTlem3  23943  ptcmplem3  23948  ptcmplem4  23949  ptcmplem5  23950  cnextfun  23958  tmdgsum2  23990  symgtgp  24000  tsmsval2  24024  tsmsgsum  24033  utoptop  24129  ismet2  24228  blin  24316  metss2lem  24406  methaus  24415  met1stc  24416  met2ndci  24417  prdsxmslem2  24424  metcnp3  24435  metcnpi3  24441  metustto  24448  metustfbas  24452  nlmvscn  24582  nrginvrcn  24587  xrsxmet  24705  reconnlem1  24722  reconn  24724  xrge0tsms  24730  xmetdcn2  24733  metdscn  24752  addcnlem  24760  fsumcn  24768  cnheiborlem  24860  cnheibor  24861  bndth  24864  lebnum  24870  nmoleub2lem2  25023  ipcn  25153  iscmet3  25200  caubl  25215  rrxdstprj1  25316  minveclem3b  25335  minveclem7  25342  pjthlem2  25345  pmltpc  25358  volfiniun  25455  ioombl1  25470  dyadss  25502  dyaddisjlem  25503  dyadmax  25506  dyadmbllem  25507  opnmbllem  25509  itg1addlem2  25605  itg10a  25618  mbfi1fseqlem6  25628  itg2seq  25650  itg2monolem1  25658  itg2gt0  25668  itgfsum  25735  limcfval  25780  ellimc2  25785  ellimc3  25787  limcres  25794  limciun  25802  dvres  25819  dveflem  25890  rolle  25901  dvlip2  25907  c1liplem1  25908  dvgt0lem1  25914  dvgt0  25916  dvlt0  25917  dvne0  25923  dvfsumrlimge0  25944  ftc1lem6  25955  itgsubst  25963  mdegmullem  25990  ply1domn  26036  ply1divex  26049  fta1g  26082  fta1b  26084  plyf  26110  dgrlem  26141  coeid  26150  plydivalg  26214  aannenlem1  26243  aalioulem3  26249  aalioulem6  26252  abelthlem8  26356  efif1olem4  26461  chordthm  26754  xrlimcnp  26885  jensen  26906  lgamcvglem  26957  lgamcvg2  26972  sqf11  27056  fsumvma2  27132  perfectlem2  27148  lgsdilem  27242  lgsquad2lem2  27303  lgsquad3  27305  2sqlem5  27340  2sqlem9  27345  2sqb  27350  rpvmasumlem  27405  dchrisum0flb  27428  dchrisum0  27438  pntpbnd  27506  pntibndlem3  27510  pntleml  27529  nolt02o  27614  nosupbday  27624  nosupbnd2  27635  noinfbday  27639  noinfbnd2  27650  noetasuplem4  27655  noetainflem4  27659  noetalem1  27660  conway  27718  slerec  27738  sltlpss  27826  addsprop  27890  bdayon  28180  n0sfincut  28253  eucliddivs  28272  remulscllem2  28359  tgjustc1  28409  tgjustc2  28410  legov  28519  legtrid  28525  tglinethru  28570  tglnpt2  28575  tglineintmo  28576  mirreu3  28588  perpcom  28647  colperpexlem3  28666  mideu  28672  opphllem1  28681  hlpasch  28690  lnopp2hpgb  28697  trgcopy  28738  brcgr  28834  brbtwn2  28839  colinearalg  28844  axsegcon  28861  axeuclidlem  28896  axcontlem9  28906  ecgrtg  28917  elntg  28918  eengtrkg  28920  upgr1eopALT  29051  usgredg4  29151  subuhgr  29220  subumgr  29222  usgr2wspthon  29902  clwlkclwwlkf1  29946  eupth2lems  30174  n4cyclfrgr  30227  vacn  30630  blocni  30741  ubthlem3  30808  minvecolem7  30819  chocunii  31237  pjhthmo  31238  pjhthlem2  31328  kbass5  32056  mdsymlem5  32343  foresf1o  32440  fcobij  32652  xrofsup  32697  mgcoval  32919  mgcf1o  32936  xrge0tsmsd  33009  symgcntz  33049  archirngz  33150  archiabllem2a  33155  isarchiofld  33302  prmidl2  33419  constrelextdg2  33744  smatrcl  33793  reff  33836  ordtconnlem1  33921  qqhval2  33979  volmeas  34228  fiunelcarsg  34314  ballotlemfc0  34491  ballotlemfcc  34492  signstfvneq0  34570  derangenlem  35165  erdsze2lem1  35197  pconnconn  35225  connpconn  35229  cvxsconn  35237  cvmliftmolem2  35276  cvmliftmo  35278  cvmlift2lem10  35306  cvmlift2lem12  35308  cvmlift3lem7  35319  mrsubff1  35508  msubff1  35550  r1peuqusdeg1  35637  ifscgr  36039  cgrxfr  36050  btwnconn1lem13  36094  btwnconn1lem14  36095  outsideofeq  36125  ellines  36147  finminlem  36313  fnejoin2  36364  weiunso  36461  unbdqndv2  36506  irrdiff  37321  poimirlem13  37634  poimirlem14  37635  poimirlem32  37653  opnmbllem0  37657  mblfinlem3  37660  itg2addnclem  37672  itg2addnc  37675  ftc1cnnc  37693  upixp  37730  filbcmb  37741  sstotbnd2  37775  isbnd3  37785  prdsbnd2  37796  cntotbnd  37797  ismtyima  37804  bfp  37825  rrncmslem  37833  unichnidl  38032  lshpcmp  38988  islshpat  39017  lfl0f  39069  ishlat3N  39354  3dim1  39468  islvol5  39580  lvoli2  39582  lncvrelatN  39782  pclfinclN  39951  pexmidlem8N  39978  idltrn  40151  cdleme42keg  40487  cdleme42mgN  40489  cdlemf2  40563  cdlemg2cex  40592  trlcoat  40724  dihopelvalcpre  41249  dih1dimatlem  41330  dihjatcclem4  41422  lcfl7N  41502  lcfrlem9  41551  mapdh9a  41790  hdmapglem7  41930  aks4d1p8  42082  isprimroot  42088  evl1gprodd  42112  sticksstones11  42151  grpods  42189  aks5lem8  42196  renegeulemv  42363  sn-subeu  42422  remulinvcom  42428  imacrhmcl  42509  fidomncyc  42530  fsuppind  42585  fsuppssind  42588  mhpind  42589  prjspertr  42600  prjspreln0  42604  flt4lem7  42654  nna4b4nsq  42655  nacsfix  42707  mzpsubst  42743  mzpcompact2lem  42746  eldioph2lem2  42756  eldioph2  42757  eldioph2b  42758  diophin  42767  diophun  42768  irrapxlem3  42819  irrapxlem5  42821  pell1234qrreccl  42849  pell1234qrmulcl  42850  pell14qrdich  42864  pell1qrge1  42865  pell1qrgaplem  42868  monotuz  42937  acongtr  42974  acongrep  42976  jm2.23  42992  jm2.26a  42996  jm2.26lem3  42997  jm2.26  42998  jm2.27  43004  wepwsolem  43038  fnwe2lem2  43047  kelac1  43059  kercvrlsm  43079  hbtlem5  43124  hbt  43126  mpaaeu  43146  cantnfresb  43320  onmcl  43327  tfsconcatun  43333  tfsconcatfn  43334  tfsconcatfv1  43335  tfsconcatfv2  43336  naddcnff  43358  rfovcnvf1od  44000  mnurndlem1  44277  cncmpmax  45033  rfcnnnub  45037  disjxp1  45070  iccintsng  45528  fprodcn  45605  lptioo2  45636  lptioo1  45637  limclner  45656  stoweidlem31  46036  stoweidlem34  46039  stoweidlem35  46040  stoweidlem49  46054  stoweidlem59  46064  stoweidlem62  46067  fourierdlem60  46171  fourierdlem61  46172  fourierdlem87  46198  iundjiun  46465  ismeannd  46472  hoidmvle  46605  smfsuplem2  46817  2reu8i  47118  prproropf1olem2  47509  paireqne  47516  perfectALTVlem2  47727  mogoldbb  47790  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  grimedg  47939  scmsuppss  48363  lindslinindsimp2lem5  48455  elfzolborelfzop1  48512  elbigolo1  48550  itschlc0xyqsol1  48759  itschlc0xyqsol  48760  iccdisj  48890  toslat  48974  iinfssclem3  49049  iinfssc  49050  iinfsubc  49051  imasubc3  49149  upciclem4  49162  uppropd  49174  natoppf  49222  tposcurf1  49292  fuco22  49332  fuco22natlem  49338  functhinclem4  49440  arweuthinc  49522