Theorem simplrr 536

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

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  rmob  3082  disjiun  4029  isotr  5866  riota5f  5905  tfrexlem  6401  tfrcl  6431  nnsucuniel  6562  pw2f1odclem  6904  fopwdom  6906  dif1enen  6950  fisbth  6953  fin0  6955  fin0or  6956  diffisn  6963  finexdc  6972  fientri3  6985  unfidisj  6992  undifdc  6994  ssfirab  7006  fnfi  7011  iunfidisj  7021  dcfi  7056  ordiso2  7110  difinfinf  7176  ctmlemr  7183  exmidfodomrlemr  7281  2omotaplemap  7340  cc2lem  7349  cc3  7351  addcmpblnq  7451  mulcmpblnq  7452  ordpipqqs  7458  ltexnqq  7492  addcmpblnq0  7527  mulcmpblnq0  7528  prmu  7562  addlocpr  7620  prmuloc  7650  prmuloc2  7651  ltaddpr  7681  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemloc  7691  ltexprlemrl  7694  ltexprlemru  7696  addcanprleml  7698  addcanprlemu  7699  aptiprleml  7723  aptiprlemu  7724  ltmprr  7726  cauappcvgprlemloc  7736  archrecpr  7748  caucvgprlemloc  7759  caucvgprprlemloc  7787  caucvgprprlemexbt  7790  suplocexprlemdisj  7804  suplocexprlemloc  7805  addcmpblnr  7823  mulcmpblnrlemg  7824  mulcmpblnr  7825  ltsrprg  7831  mulgt0sr  7862  caucvgsrlemgt1  7879  suplocsrlemb  7890  axmulcl  7950  axarch  7975  axcaucvglemres  7983  axpre-suploclemres  7985  axpre-suploc  7986  readdcan  8183  cnegexlem1  8218  negeu  8234  add20  8518  apreap  8631  cru  8646  apsym  8650  apcotr  8651  apadd1  8652  apneg  8655  mulext1  8656  divdivdivap  8757  ltmul12a  8904  lemul12a  8906  lt2mul2div  8923  ledivdiv  8934  lediv12a  8938  qapne  9730  xleadd1a  9965  ixxss12  9998  ioodisj  10085  fz0fzelfz0  10219  zsupcllemstep  10336  zsupssdc  10345  qtri3or  10347  exbtwnzlemstep  10354  exbtwnzlemex  10356  exbtwnz  10357  rebtwn2zlemstep  10359  rebtwn2z  10361  qbtwnre  10363  btwnzge0  10407  iseqf1olemqf1o  10615  mulexpzap  10688  leexp1a  10703  expnbnd  10772  hashen  10893  fihashdom  10912  hashun  10914  zfz1iso  10950  cjap  11088  cvg1nlemres  11167  rsqrmo  11209  abs3lem  11293  cau3lem  11296  rexanre  11402  xrmaxltsup  11440  climcau  11529  sumeq2  11541  summodc  11565  fsum3cvg3  11578  fsum2d  11617  prodeq2  11739  prodmodclem2  11759  fprod2d  11805  eirrap  11960  addmodlteqALT  12041  divalglemeunn  12103  divalglemeuneg  12105  bezoutlemnewy  12188  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlembi  12197  bezoutlemeu  12199  rpdvds  12292  isprm5lem  12334  isprm6  12340  pw2dvdslemn  12358  pw2dvdseu  12361  sqrt2irrap  12373  pythagtriplem2  12460  pythagtrip  12477  pclemub  12481  pcqmul  12497  pcexp  12503  pcneg  12519  pcprmpw2  12527  pcadd  12534  pcmpt  12537  4sqlem13m  12597  ennnfonelemrnh  12658  ennnfonelemnn0  12664  ctinfomlemom  12669  ctiunctlemfo  12681  nninfdclemf1  12694  imasival  13008  gsumpropd2  13095  sgrppropd  13115  ismndd  13139  mndpropd  13142  mhmeql  13194  mhmmnd  13322  issubg4m  13399  ssnmz  13417  conjnmzb  13486  rngpropd  13587  ringpropd  13670  islmod  13923  psrval  14296  restbasg  14488  cnrest2  14556  cnpdis  14562  lmtopcnp  14570  txcnp  14591  txlm  14599  ismet2  14674  blininf  14744  metss2lem  14817  xmettxlem  14829  xmettx  14830  metcnp3  14831  metcnpi3  14837  addcncntoplem  14881  fsumcncntop  14887  mulcncf  14928  dedekindeulemuub  14937  dedekindeu  14943  dedekindicclemuub  14946  ivthinclemlopn  14956  ivthinclemuopn  14958  ivthinclemloc  14961  ivthinc  14963  ivthdichlem  14971  limcimo  14985  limccnp2cntop  14997  plyf  15057  plyco  15079  plycj  15081  plyrecj  15083  dvply2g  15086  logbgcd1irrap  15290  perfectlem2  15320  lgsdilem  15352  lgsquad2lem2  15407  lgsquad3  15409  2sqlem5  15444  2sqlem9  15449  2omap  15726  qdencn  15758  apdiff  15779