Theorem simplrr 538

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  3135  disjiun  4103  isotr  5988  riota5f  6029  tfrexlem  6564  tfrcl  6594  nnsucuniel  6727  pw2f1odclem  7086  fopwdom  7088  dif1enen  7136  fisbth  7139  fin0  7141  fin0or  7142  diffisn  7149  fidcen  7155  finexdc  7159  elssdc  7161  fientri3  7174  unfidisj  7181  undifdc  7183  ssfirab  7196  fnfi  7202  iunfidisj  7212  mapfi  7213  fissfi  7215  dcfi  7267  2omap  7268  ordiso2  7325  difinfinf  7391  ctmlemr  7398  exmidfodomrlemr  7504  2omotaplemap  7567  cc2lem  7576  cc3  7578  addcmpblnq  7678  mulcmpblnq  7679  ordpipqqs  7685  ltexnqq  7719  addcmpblnq0  7754  mulcmpblnq0  7755  prmu  7789  addlocpr  7847  prmuloc  7877  prmuloc2  7878  ltaddpr  7908  ltexprlemopl  7912  ltexprlemopu  7914  ltexprlemloc  7918  ltexprlemrl  7921  ltexprlemru  7923  addcanprleml  7925  addcanprlemu  7926  aptiprleml  7950  aptiprlemu  7951  ltmprr  7953  cauappcvgprlemloc  7963  archrecpr  7975  caucvgprlemloc  7986  caucvgprprlemloc  8014  caucvgprprlemexbt  8017  suplocexprlemdisj  8031  suplocexprlemloc  8032  addcmpblnr  8050  mulcmpblnrlemg  8051  mulcmpblnr  8052  ltsrprg  8058  mulgt0sr  8089  caucvgsrlemgt1  8106  suplocsrlemb  8117  axmulcl  8177  axarch  8202  axcaucvglemres  8210  axpre-suploclemres  8212  axpre-suploc  8213  readdcan  8409  cnegexlem1  8444  negeu  8460  add20  8744  apreap  8857  cru  8872  apsym  8876  apcotr  8877  apadd1  8878  apneg  8881  mulext1  8882  divdivdivap  8983  ltmul12a  9130  lemul12a  9132  lt2mul2div  9149  ledivdiv  9160  lediv12a  9164  qapne  9967  xleadd1a  10202  ixxss12  10235  ioodisj  10322  fz0fzelfz0  10457  zsupcllemstep  10585  zsupssdc  10594  qtri3or  10596  exbtwnzlemstep  10603  exbtwnzlemex  10605  exbtwnz  10606  rebtwn2zlemstep  10608  rebtwn2z  10610  qbtwnre  10612  btwnzge0  10656  iseqf1olemqf1o  10864  mulexpzap  10937  leexp1a  10952  expnbnd  11021  hashen  11142  fihashdom  11162  hashun  11164  zfz1iso  11206  swrdccat  11420  reuccatpfxs1  11432  cjap  11584  cvg1nlemres  11663  rsqrmo  11705  abs3lem  11789  cau3lem  11792  rexanre  11898  xrmaxltsup  11936  climcau  12025  sumeq2  12037  summodc  12062  fsum3cvg3  12075  fsum2d  12114  prodeq2  12236  prodmodclem2  12256  fprod2d  12302  eirrap  12457  addmodlteqALT  12538  divalglemeunn  12600  divalglemeuneg  12602  bezoutlemnewy  12685  bezoutlemstep  12686  bezoutlemmain  12687  bezoutlembi  12694  bezoutlemeu  12696  rpdvds  12789  isprm5lem  12831  isprm6  12837  pw2dvdslemn  12855  pw2dvdseu  12858  sqrt2irrap  12870  pythagtriplem2  12957  pythagtrip  12974  pclemub  12978  pcqmul  12994  pcexp  13000  pcneg  13016  pcprmpw2  13024  pcadd  13031  pcmpt  13034  4sqlem13m  13094  ennnfonelemrnh  13156  ennnfonelemnn0  13162  ctinfomlemom  13167  ctiunctlemfo  13179  nninfdclemf1  13192  imasival  13508  gsumpropd2  13595  sgrppropd  13615  ismndd  13639  mndpropd  13642  mhmeql  13694  mhmmnd  13822  issubg4m  13899  ssnmz  13917  conjnmzb  13986  rngpropd  14088  ringpropd  14171  islmod  14426  psrval  14801  restbasg  15020  cnrest2  15088  cnpdis  15094  lmtopcnp  15102  txcnp  15123  txlm  15131  ismet2  15206  blininf  15276  metss2lem  15349  xmettxlem  15361  xmettx  15362  metcnp3  15363  metcnpi3  15369  addcncntoplem  15413  fsumcncntop  15419  mulcncf  15460  dedekindeulemuub  15469  dedekindeu  15475  dedekindicclemuub  15478  ivthinclemlopn  15488  ivthinclemuopn  15490  ivthinclemloc  15493  ivthinc  15495  ivthdichlem  15503  limcimo  15517  limccnp2cntop  15529  plyf  15589  plyco  15611  plycj  15613  plyrecj  15615  dvply2g  15618  logbgcd1irrap  15822  perfectlem2  15855  lgsdilem  15887  lgsquad2lem2  15942  lgsquad3  15944  2sqlem5  15979  2sqlem9  15984  usgredg4  16197  usgr1vr  16230  subuhgr  16254  subumgr  16256  clwwlknonex2lem2  16420  eupth2lemsfi  16460  depindlem3  16490  qdencn  16794  apdiff  16819  qdiff  16820  gfsumval  16848