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 484	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 723	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 206  df-an 396

This theorem is referenced by:  disjxiun  5067  frpomin  6228  fsnex  7135  f1prex  7136  isotr  7187  weniso  7205  riota5f  7241  fprlem2  8088  tfrlem9a  8188  oaass  8354  oeeui  8395  oaabs2  8439  resixpfo  8682  omxpenlem  8813  pw2f1olem  8816  fopwdom  8820  fofinf1o  9024  marypha1lem  9122  ordiso2  9204  oismo  9229  ixpiunwdom  9279  cantnf  9381  fseqenlem1  9711  iunfictbso  9801  dfac12lem2  9831  dfac12lem3  9832  infunsdom1  9900  infpssrlem5  9994  fin23lem24  10009  isf32lem2  10041  isf32lem4  10043  isf34lem4  10064  fin1a2lem12  10098  fin1a2lem13  10099  ttukeylem6  10201  fpwwe2lem11  10328  fpwwe2lem12  10329  fpwwe2  10330  winalim2  10383  wunex2  10425  tskord  10467  prlem934  10720  mulcmpblnr  10758  dedekind  11068  addid1  11085  cnegex  11086  negeu  11141  add20  11417  divdivdiv  11606  ltmul12a  11761  lemul12a  11763  lediv12a  11798  supaddc  11872  supmul1  11874  cru  11895  uzwo3  12612  xleadd1a  12916  xmullem  12927  xmulgt0  12946  xlemul1a  12951  ixxun  13024  ixxss12  13028  ioodisj  13143  fz0fzelfz0  13291  mulexpz  13751  rpexpmord  13814  leexp1a  13821  expmulnbnd  13878  hashf1  14099  fi1uzind  14139  brfi1indALT  14142  swrdccat  14376  reuccatpfxs1  14388  abs3lem  14978  rexanre  14986  cau3lem  14994  limsupgre  15118  limsupbnd2  15120  o1lo1  15174  rlimclim1  15182  rlimclim  15183  rlimcn1  15225  rlimcn3  15227  o1of2  15250  o1rlimmul  15256  lo1add  15264  lo1mul  15265  isercolllem1  15304  climcau  15310  caucvgrlem  15312  caucvgb  15319  summolem2  15356  summo  15357  modfsummod  15434  o1fsum  15453  prodmolem2  15573  addmodlteqALT  15962  rpdvds  16293  isprm5  16340  isprm6  16347  pclem  16467  pcqmul  16482  pcexp  16488  pcneg  16503  pcprmpw2  16511  pcadd  16518  pcmpt  16521  4sqlem13  16586  vdwlem2  16611  vdwlem7  16616  vdwlem12  16621  ramval  16637  ramub2  16643  ramz2  16653  ramcl  16658  cshwshashlem2  16726  imasval  17139  imasdsval  17143  mreexexd  17274  acsfn  17285  issubc3  17480  idfucl  17512  funcres2c  17533  isnat  17579  fucpropd  17611  xpcval  17810  xpcco  17816  prfval  17832  evlf2  17852  evlfcl  17856  curf12  17861  curf1cl  17862  curf2  17863  curfcl  17866  curf2ndf  17881  hof2val  17890  hofcl  17893  hofpropd  17901  yonedalem4a  17909  yonedainv  17915  drsdirfi  17938  pospo  17978  poslubmo  18044  posglbmo  18045  isipodrs  18170  acsinfd  18189  gsumvalx  18275  gsumpropd2lem  18278  ismndd  18322  mndpropd  18325  mhmeql  18379  mndind  18381  frmdup3lem  18420  mhmmnd  18612  issubg4  18689  ssnmz  18709  conjnmzb  18784  f1otrspeq  18970  psgneu  19029  pgpfi  19125  sylow2blem3  19142  slwhash  19144  fislw  19145  sylow3lem2  19148  lsmdisj2  19203  pj1eu  19217  efgredlem  19268  frgpuplem  19293  gexex  19369  frgpnabl  19391  dprdfadd  19538  dpjidcl  19576  pgpfac1lem3  19595  pgpfaclem3  19601  ablfac2  19607  ablsimpgcygd  19624  ablsimpgfind  19628  ablsimpgprmd  19633  ringpropd  19736  islmhm2  20215  lmhmpropd  20250  lbsextlem4  20338  prmirredlem  20606  psgndiflemA  20718  lsmcss  20809  uvcf1  20909  frlmsslsp  20913  frlmup1  20915  assapropd  20986  psrval  21028  evlslem1  21202  mamucl  21458  mamuass  21459  mamudi  21460  mamudir  21461  mamuvs1  21462  mamuvs2  21463  mamulid  21498  mamurid  21499  dmatsubcl  21555  dmatmulcl  21557  scmatscm  21570  marrepval  21619  marepveval  21625  mdetunilem7  21675  gsummatr01lem4  21715  cpmatmcllem  21775  mat2pmatf1  21786  mat2pmatlin  21792  decpmatmul  21829  pm2mpmhmlem2  21876  chpidmat  21904  pptbas  22066  toponmre  22152  restbas  22217  iscncl  22328  cnrest2  22345  cnpdis  22352  lmcnp  22363  dishaus  22441  cmpcovf  22450  tgcmp  22460  dfconn2  22478  clsconn  22489  2ndcctbss  22514  dis2ndc  22519  1stccnp  22521  islly2  22543  cldllycmp  22554  locfincmp  22585  comppfsc  22591  kgentopon  22597  txcls  22663  ptpjopn  22671  dfac14  22677  xkoccn  22678  txcnp  22679  txcmpb  22703  txlm  22707  xkopt  22714  xkoco1cn  22716  xkoco2cn  22717  qtopcn  22773  qtoprest  22776  regr1lem2  22799  xkocnv  22873  qtophmeo  22876  fmfnfmlem4  23016  hausflim  23040  hauspwpwf1  23046  fclscmp  23089  alexsublem  23103  alexsubALTlem2  23107  alexsubALTlem3  23108  ptcmplem3  23113  ptcmplem4  23114  ptcmplem5  23115  cnextfun  23123  tmdgsum2  23155  symgtgp  23165  tsmsval2  23189  tsmsgsum  23198  utoptop  23294  ismet2  23394  blin  23482  metss2lem  23573  methaus  23582  met1stc  23583  met2ndci  23584  prdsxmslem2  23591  metcnp3  23602  metcnpi3  23608  metustto  23615  metustfbas  23619  nlmvscn  23757  nrginvrcn  23762  xrsxmet  23878  reconnlem1  23895  reconn  23897  xrge0tsms  23903  xmetdcn2  23906  metdscn  23925  addcnlem  23933  fsumcn  23939  cnheiborlem  24023  cnheibor  24024  bndth  24027  lebnum  24033  nmoleub2lem2  24185  ipcn  24315  iscmet3  24362  caubl  24377  rrxdstprj1  24478  minveclem3b  24497  minveclem7  24504  pjthlem2  24507  pmltpc  24519  volfiniun  24616  ioombl1  24631  dyadss  24663  dyaddisjlem  24664  dyadmax  24667  dyadmbllem  24668  opnmbllem  24670  itg1addlem2  24766  itg10a  24780  mbfi1fseqlem6  24790  itg2seq  24812  itg2monolem1  24820  itg2gt0  24830  itgfsum  24896  limcfval  24941  ellimc2  24946  ellimc3  24948  limcres  24955  limciun  24963  dvres  24980  dveflem  25048  rolle  25059  dvlip2  25064  c1liplem1  25065  dvgt0lem1  25071  dvgt0  25073  dvlt0  25074  dvne0  25080  dvfsumrlimge0  25099  ftc1lem6  25110  itgsubst  25118  mdegmullem  25148  ply1domn  25193  ply1divex  25206  fta1g  25237  fta1b  25239  plyf  25264  dgrlem  25295  coeid  25304  plydivalg  25364  aannenlem1  25393  aalioulem3  25399  aalioulem6  25402  abelthlem8  25503  efif1olem4  25606  chordthm  25892  xrlimcnp  26023  jensen  26043  lgamcvglem  26094  lgamcvg2  26109  sqf11  26193  fsumvma2  26267  perfectlem2  26283  lgsdilem  26377  lgsquad2lem2  26438  lgsquad3  26440  2sqlem5  26475  2sqlem9  26480  2sqb  26485  rpvmasumlem  26540  dchrisum0flb  26563  dchrisum0  26573  pntpbnd  26641  pntibndlem3  26645  pntleml  26664  tgjustc1  26740  tgjustc2  26741  legov  26850  legtrid  26856  tglinethru  26901  tglnpt2  26906  tglineintmo  26907  mirreu3  26919  perpcom  26978  colperpexlem3  26997  mideu  27003  opphllem1  27012  hlpasch  27021  lnopp2hpgb  27028  trgcopy  27069  brcgr  27171  brbtwn2  27176  colinearalg  27181  axsegcon  27198  axeuclidlem  27233  axcontlem9  27243  ecgrtg  27254  elntg  27255  eengtrkg  27257  upgr1eopALT  27390  usgredg4  27487  subuhgr  27556  subumgr  27558  usgr2wspthon  28231  clwlkclwwlkf1  28275  eupth2lems  28503  n4cyclfrgr  28556  vacn  28957  blocni  29068  ubthlem3  29135  minvecolem7  29146  chocunii  29564  pjhthmo  29565  pjhthlem2  29655  kbass5  30383  mdsymlem5  30670  foresf1o  30751  fcobij  30959  xrofsup  30992  mgcoval  31166  mgcf1o  31183  xrge0tsmsd  31219  symgcntz  31256  archirngz  31345  archiabllem2a  31350  isarchiofld  31418  prmidl2  31518  smatrcl  31648  reff  31691  ordtconnlem1  31776  qqhval2  31832  volmeas  32099  fiunelcarsg  32183  ballotlemfc0  32359  ballotlemfcc  32360  signstfvneq0  32451  derangenlem  33033  erdsze2lem1  33065  pconnconn  33093  connpconn  33097  cvxsconn  33105  cvmliftmolem2  33144  cvmliftmo  33146  cvmlift2lem10  33174  cvmlift2lem12  33176  cvmlift3lem7  33187  mrsubff1  33376  msubff1  33418  ttrclss  33706  frxp2  33718  frxp3  33724  poseq  33729  naddssim  33764  nolt02o  33825  nosupbday  33835  nosupbnd2  33846  noinfbday  33850  noinfbnd2  33861  noetasuplem4  33866  noetainflem4  33870  noetalem1  33871  conway  33920  slerec  33940  sltlpss  34014  ifscgr  34273  cgrxfr  34284  btwnconn1lem13  34328  btwnconn1lem14  34329  outsideofeq  34359  ellines  34381  finminlem  34434  fnejoin2  34485  unbdqndv2  34618  irrdiff  35424  poimirlem13  35717  poimirlem14  35718  poimirlem32  35736  opnmbllem0  35740  mblfinlem3  35743  itg2addnclem  35755  itg2addnc  35758  ftc1cnnc  35776  upixp  35814  filbcmb  35825  sstotbnd2  35859  isbnd3  35869  prdsbnd2  35880  cntotbnd  35881  ismtyima  35888  bfp  35909  rrncmslem  35917  unichnidl  36116  lshpcmp  36929  islshpat  36958  lfl0f  37010  ishlat3N  37295  3dim1  37408  islvol5  37520  lvoli2  37522  lncvrelatN  37722  pclfinclN  37891  pexmidlem8N  37918  idltrn  38091  cdleme42keg  38427  cdleme42mgN  38429  cdlemf2  38503  cdlemg2cex  38532  trlcoat  38664  dihopelvalcpre  39189  dih1dimatlem  39270  dihjatcclem4  39362  lcfl7N  39442  lcfrlem9  39491  mapdh9a  39730  hdmapglem7  39870  aks4d1p8  40023  sticksstones11  40040  fsuppind  40202  fsuppssind  40205  mhpind  40206  mhphf  40208  renegeulemv  40272  sn-subeu  40329  remulinvcom  40335  itrere  40357  retire  40358  prjspertr  40365  prjspreln0  40369  flt4lem7  40412  nna4b4nsq  40413  nacsfix  40450  mzpsubst  40486  mzpcompact2lem  40489  eldioph2lem2  40499  eldioph2  40500  eldioph2b  40501  diophin  40510  diophun  40511  irrapxlem3  40562  irrapxlem5  40564  pell1234qrreccl  40592  pell1234qrmulcl  40593  pell14qrdich  40607  pell1qrge1  40608  pell1qrgaplem  40611  monotuz  40679  acongtr  40716  acongrep  40718  jm2.23  40734  jm2.26a  40738  jm2.26lem3  40739  jm2.26  40740  jm2.27  40746  wepwsolem  40783  fnwe2lem2  40792  kelac1  40804  kercvrlsm  40824  hbtlem5  40869  hbt  40871  mpaaeu  40891  rfovcnvf1od  41501  mnurndlem1  41788  cncmpmax  42464  rfcnnnub  42468  disjxp1  42506  iccintsng  42951  fprodcn  43031  lptioo2  43062  lptioo1  43063  limclner  43082  stoweidlem31  43462  stoweidlem34  43465  stoweidlem35  43466  stoweidlem49  43480  stoweidlem59  43490  stoweidlem62  43493  fourierdlem60  43597  fourierdlem61  43598  fourierdlem87  43624  iundjiun  43888  ismeannd  43895  hoidmvle  44028  smfsuplem2  44232  2reu8i  44492  prproropf1olem2  44844  paireqne  44851  perfectALTVlem2  45062  mogoldbb  45125  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  isomgrtrlem  45178  mgmhmeql  45245  mndpsuppss  45595  scmsuppss  45596  lindslinindsimp2lem5  45691  elfzolborelfzop1  45748  elbigolo1  45791  itschlc0xyqsol1  46000  itschlc0xyqsol  46001  iccdisj  46080  toslat  46156  functhinclem4  46213