Theorem simplrr 526

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  rmob  3043  disjiun  3977  isotr  5784  riota5f  5822  tfrexlem  6302  tfrcl  6332  nnsucuniel  6463  fopwdom  6802  dif1enen  6846  fisbth  6849  fin0  6851  fin0or  6852  diffisn  6859  finexdc  6868  fientri3  6880  unfidisj  6887  undifdc  6889  ssfirab  6899  fnfi  6902  iunfidisj  6911  dcfi  6946  ordiso2  7000  difinfinf  7066  ctmlemr  7073  exmidfodomrlemr  7158  cc2lem  7207  cc3  7209  addcmpblnq  7308  mulcmpblnq  7309  ordpipqqs  7315  ltexnqq  7349  addcmpblnq0  7384  mulcmpblnq0  7385  prmu  7419  addlocpr  7477  prmuloc  7507  prmuloc2  7508  ltaddpr  7538  ltexprlemopl  7542  ltexprlemopu  7544  ltexprlemloc  7548  ltexprlemrl  7551  ltexprlemru  7553  addcanprleml  7555  addcanprlemu  7556  aptiprleml  7580  aptiprlemu  7581  ltmprr  7583  cauappcvgprlemloc  7593  archrecpr  7605  caucvgprlemloc  7616  caucvgprprlemloc  7644  caucvgprprlemexbt  7647  suplocexprlemdisj  7661  suplocexprlemloc  7662  addcmpblnr  7680  mulcmpblnrlemg  7681  mulcmpblnr  7682  ltsrprg  7688  mulgt0sr  7719  caucvgsrlemgt1  7736  suplocsrlemb  7747  axmulcl  7807  axarch  7832  axcaucvglemres  7840  axpre-suploclemres  7842  axpre-suploc  7843  readdcan  8038  cnegexlem1  8073  negeu  8089  add20  8372  apreap  8485  cru  8500  apsym  8504  apcotr  8505  apadd1  8506  apneg  8509  mulext1  8510  divdivdivap  8609  ltmul12a  8755  lemul12a  8757  lt2mul2div  8774  ledivdiv  8785  lediv12a  8789  qapne  9577  xleadd1a  9809  ixxss12  9842  ioodisj  9929  fz0fzelfz0  10062  qtri3or  10178  exbtwnzlemstep  10183  exbtwnzlemex  10185  exbtwnz  10186  rebtwn2zlemstep  10188  rebtwn2z  10190  qbtwnre  10192  btwnzge0  10235  iseqf1olemqf1o  10428  mulexpzap  10495  leexp1a  10510  expnbnd  10578  hashen  10697  fihashdom  10716  hashun  10718  zfz1iso  10754  cjap  10848  cvg1nlemres  10927  rsqrmo  10969  abs3lem  11053  cau3lem  11056  rexanre  11162  xrmaxltsup  11199  climcau  11288  sumeq2  11300  summodc  11324  fsum3cvg3  11337  fsum2d  11376  prodeq2  11498  prodmodclem2  11518  fprod2d  11564  eirrap  11718  addmodlteqALT  11797  divalglemeunn  11858  divalglemeuneg  11860  zsupcllemstep  11878  zsupssdc  11887  bezoutlemnewy  11929  bezoutlemstep  11930  bezoutlemmain  11931  bezoutlembi  11938  bezoutlemeu  11940  rpdvds  12031  isprm5lem  12073  isprm6  12079  pw2dvdslemn  12097  pw2dvdseu  12100  sqrt2irrap  12112  pythagtriplem2  12198  pythagtrip  12215  pclemub  12219  pcqmul  12235  pcexp  12241  pcneg  12256  pcprmpw2  12264  pcadd  12271  pcmpt  12273  ennnfonelemrnh  12349  ennnfonelemnn0  12355  ctinfomlemom  12360  ctiunctlemfo  12372  nninfdclemf1  12385  restbasg  12808  cnrest2  12876  cnpdis  12882  lmtopcnp  12890  txcnp  12911  txlm  12919  ismet2  12994  blininf  13064  metss2lem  13137  xmettxlem  13149  xmettx  13150  metcnp3  13151  metcnpi3  13157  addcncntoplem  13191  fsumcncntop  13196  mulcncf  13231  dedekindeulemuub  13235  dedekindeu  13241  dedekindicclemuub  13244  ivthinclemlopn  13254  ivthinclemuopn  13256  ivthinclemloc  13259  ivthinc  13261  limcimo  13274  limccnp2cntop  13286  logbgcd1irrap  13528  lgsdilem  13568  2sqlem5  13595  2sqlem9  13600  qdencn  13906  apdiff  13927