Theorem simplrr 525

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 480	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  3001  disjiun  3924  isotr  5717  riota5f  5754  tfrexlem  6231  tfrcl  6261  nnsucuniel  6391  fopwdom  6730  dif1enen  6774  fisbth  6777  fin0  6779  fin0or  6780  diffisn  6787  finexdc  6796  fientri3  6803  unfidisj  6810  undifdc  6812  ssfirab  6822  fnfi  6825  iunfidisj  6834  ordiso2  6920  difinfinf  6986  ctmlemr  6993  exmidfodomrlemr  7058  addcmpblnq  7175  mulcmpblnq  7176  ordpipqqs  7182  ltexnqq  7216  addcmpblnq0  7251  mulcmpblnq0  7252  prmu  7286  addlocpr  7344  prmuloc  7374  prmuloc2  7375  ltaddpr  7405  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemloc  7415  ltexprlemrl  7418  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  aptiprleml  7447  aptiprlemu  7448  ltmprr  7450  cauappcvgprlemloc  7460  archrecpr  7472  caucvgprlemloc  7483  caucvgprprlemloc  7511  caucvgprprlemexbt  7514  suplocexprlemdisj  7528  suplocexprlemloc  7529  addcmpblnr  7547  mulcmpblnrlemg  7548  mulcmpblnr  7549  ltsrprg  7555  mulgt0sr  7586  caucvgsrlemgt1  7603  suplocsrlemb  7614  axmulcl  7674  axarch  7699  axcaucvglemres  7707  axpre-suploclemres  7709  axpre-suploc  7710  readdcan  7902  cnegexlem1  7937  negeu  7953  add20  8236  apreap  8349  cru  8364  apsym  8368  apcotr  8369  apadd1  8370  apneg  8373  mulext1  8374  divdivdivap  8473  ltmul12a  8618  lemul12a  8620  lt2mul2div  8637  ledivdiv  8648  lediv12a  8652  qapne  9431  xleadd1a  9656  ixxss12  9689  ioodisj  9776  fz0fzelfz0  9904  qtri3or  10020  exbtwnzlemstep  10025  exbtwnzlemex  10027  exbtwnz  10028  rebtwn2zlemstep  10030  rebtwn2z  10032  qbtwnre  10034  btwnzge0  10073  iseqf1olemqf1o  10266  mulexpzap  10333  leexp1a  10348  expnbnd  10415  hashen  10530  fihashdom  10549  hashun  10551  zfz1iso  10584  cjap  10678  cvg1nlemres  10757  rsqrmo  10799  abs3lem  10883  cau3lem  10886  rexanre  10992  xrmaxltsup  11027  climcau  11116  sumeq2  11128  summodc  11152  fsum3cvg3  11165  fsum2d  11204  prodeq2  11326  prodmodclem2  11346  eirrap  11484  addmodlteqALT  11557  divalglemeunn  11618  divalglemeuneg  11620  zsupcllemstep  11638  bezoutlemnewy  11684  bezoutlemstep  11685  bezoutlemmain  11686  bezoutlembi  11693  bezoutlemeu  11695  rpdvds  11780  isprm6  11825  pw2dvdslemn  11843  pw2dvdseu  11846  sqrt2irrap  11858  ennnfonelemrnh  11929  ennnfonelemnn0  11935  ctinfomlemom  11940  ctiunctlemfo  11952  restbasg  12337  cnrest2  12405  cnpdis  12411  lmtopcnp  12419  txcnp  12440  txlm  12448  ismet2  12523  blininf  12593  metss2lem  12666  xmettxlem  12678  xmettx  12679  metcnp3  12680  metcnpi3  12686  addcncntoplem  12720  fsumcncntop  12725  mulcncf  12760  dedekindeulemuub  12764  dedekindeu  12770  dedekindicclemuub  12773  ivthinclemlopn  12783  ivthinclemuopn  12785  ivthinclemloc  12788  ivthinc  12790  limcimo  12803  limccnp2cntop  12815  qdencn  13222