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  3100  disjiun  4055  isotr  5910  riota5f  5949  tfrexlem  6445  tfrcl  6475  nnsucuniel  6606  pw2f1odclem  6958  fopwdom  6960  dif1enen  7005  fisbth  7008  fin0  7010  fin0or  7011  diffisn  7018  finexdc  7027  fientri3  7040  unfidisj  7047  undifdc  7049  ssfirab  7061  fnfi  7066  iunfidisj  7076  dcfi  7111  ordiso2  7165  difinfinf  7231  ctmlemr  7238  exmidfodomrlemr  7343  2omotaplemap  7406  cc2lem  7415  cc3  7417  addcmpblnq  7517  mulcmpblnq  7518  ordpipqqs  7524  ltexnqq  7558  addcmpblnq0  7593  mulcmpblnq0  7594  prmu  7628  addlocpr  7686  prmuloc  7716  prmuloc2  7717  ltaddpr  7747  ltexprlemopl  7751  ltexprlemopu  7753  ltexprlemloc  7757  ltexprlemrl  7760  ltexprlemru  7762  addcanprleml  7764  addcanprlemu  7765  aptiprleml  7789  aptiprlemu  7790  ltmprr  7792  cauappcvgprlemloc  7802  archrecpr  7814  caucvgprlemloc  7825  caucvgprprlemloc  7853  caucvgprprlemexbt  7856  suplocexprlemdisj  7870  suplocexprlemloc  7871  addcmpblnr  7889  mulcmpblnrlemg  7890  mulcmpblnr  7891  ltsrprg  7897  mulgt0sr  7928  caucvgsrlemgt1  7945  suplocsrlemb  7956  axmulcl  8016  axarch  8041  axcaucvglemres  8049  axpre-suploclemres  8051  axpre-suploc  8052  readdcan  8249  cnegexlem1  8284  negeu  8300  add20  8584  apreap  8697  cru  8712  apsym  8716  apcotr  8717  apadd1  8718  apneg  8721  mulext1  8722  divdivdivap  8823  ltmul12a  8970  lemul12a  8972  lt2mul2div  8989  ledivdiv  9000  lediv12a  9004  qapne  9797  xleadd1a  10032  ixxss12  10065  ioodisj  10152  fz0fzelfz0  10286  zsupcllemstep  10411  zsupssdc  10420  qtri3or  10422  exbtwnzlemstep  10429  exbtwnzlemex  10431  exbtwnz  10432  rebtwn2zlemstep  10434  rebtwn2z  10436  qbtwnre  10438  btwnzge0  10482  iseqf1olemqf1o  10690  mulexpzap  10763  leexp1a  10778  expnbnd  10847  hashen  10968  fihashdom  10987  hashun  10989  zfz1iso  11025  swrdccat  11228  reuccatpfxs1  11240  cjap  11378  cvg1nlemres  11457  rsqrmo  11499  abs3lem  11583  cau3lem  11586  rexanre  11692  xrmaxltsup  11730  climcau  11819  sumeq2  11831  summodc  11855  fsum3cvg3  11868  fsum2d  11907  prodeq2  12029  prodmodclem2  12049  fprod2d  12095  eirrap  12250  addmodlteqALT  12331  divalglemeunn  12393  divalglemeuneg  12395  bezoutlemnewy  12478  bezoutlemstep  12479  bezoutlemmain  12480  bezoutlembi  12487  bezoutlemeu  12489  rpdvds  12582  isprm5lem  12624  isprm6  12630  pw2dvdslemn  12648  pw2dvdseu  12651  sqrt2irrap  12663  pythagtriplem2  12750  pythagtrip  12767  pclemub  12771  pcqmul  12787  pcexp  12793  pcneg  12809  pcprmpw2  12817  pcadd  12824  pcmpt  12827  4sqlem13m  12887  ennnfonelemrnh  12948  ennnfonelemnn0  12954  ctinfomlemom  12959  ctiunctlemfo  12971  nninfdclemf1  12984  imasival  13299  gsumpropd2  13386  sgrppropd  13406  ismndd  13430  mndpropd  13433  mhmeql  13485  mhmmnd  13613  issubg4m  13690  ssnmz  13708  conjnmzb  13777  rngpropd  13878  ringpropd  13961  islmod  14214  psrval  14589  restbasg  14801  cnrest2  14869  cnpdis  14875  lmtopcnp  14883  txcnp  14904  txlm  14912  ismet2  14987  blininf  15057  metss2lem  15130  xmettxlem  15142  xmettx  15143  metcnp3  15144  metcnpi3  15150  addcncntoplem  15194  fsumcncntop  15200  mulcncf  15241  dedekindeulemuub  15250  dedekindeu  15256  dedekindicclemuub  15259  ivthinclemlopn  15269  ivthinclemuopn  15271  ivthinclemloc  15274  ivthinc  15276  ivthdichlem  15284  limcimo  15298  limccnp2cntop  15310  plyf  15370  plyco  15392  plycj  15394  plyrecj  15396  dvply2g  15399  logbgcd1irrap  15603  perfectlem2  15633  lgsdilem  15665  lgsquad2lem2  15720  lgsquad3  15722  2sqlem5  15757  2sqlem9  15762  2omap  16240  qdencn  16276  apdiff  16297