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  3139  disjiun  4109  isotr  5995  riota5f  6038  tfrexlem  6578  tfrcl  6608  nnsucuniel  6741  pw2f1odclem  7100  fopwdom  7102  dif1enen  7150  fisbth  7153  fin0  7155  fin0or  7156  diffisn  7163  fidcen  7169  finexdc  7173  elssdc  7175  fientri3  7188  unfidisj  7195  undifdc  7197  ssfirab  7210  fnfi  7216  iunfidisj  7226  mapfi  7227  fissfi  7229  dcfi  7281  2omap  7282  ordiso2  7339  difinfinf  7405  ctmlemr  7412  exmidfodomrlemr  7518  2omotaplemap  7587  cc2lem  7596  cc3  7598  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  ltexnqq  7739  addcmpblnq0  7774  mulcmpblnq0  7775  prmu  7809  addlocpr  7867  prmuloc  7897  prmuloc2  7898  ltaddpr  7928  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemloc  7938  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  aptiprleml  7970  aptiprlemu  7971  ltmprr  7973  cauappcvgprlemloc  7983  archrecpr  7995  caucvgprlemloc  8006  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  suplocexprlemdisj  8051  suplocexprlemloc  8052  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  ltsrprg  8078  mulgt0sr  8109  caucvgsrlemgt1  8126  suplocsrlemb  8137  axmulcl  8197  axarch  8222  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  readdcan  8430  cnegexlem1  8465  negeu  8481  add20  8766  apreap  8879  cru  8894  apsym  8898  apcotr  8899  apadd1  8900  apneg  8903  mulext1  8904  divdivdivap  9007  ltmul12a  9154  lemul12a  9156  lt2mul2div  9173  ledivdiv  9184  lediv12a  9188  qapne  9992  xleadd1a  10228  ixxss12  10261  ioodisj  10348  fz0fzelfz0  10486  zsupcllemstep  10614  zsupssdc  10625  qtri3or  10627  exbtwnzlemstep  10634  exbtwnzlemex  10636  exbtwnz  10637  rebtwn2zlemstep  10639  rebtwn2z  10641  qbtwnre  10643  btwnzge0  10687  iseqf1olemqf1o  10895  mulexpzap  10968  leexp1a  10983  expnbnd  11053  hashen  11175  fihashdom  11195  hashun  11197  zfz1iso  11241  swrdccat  11455  reuccatpfxs1  11467  cjap  11619  cvg1nlemres  11698  rsqrmo  11740  abs3lem  11824  cau3lem  11827  rexanre  11933  xrmaxltsup  11971  climcau  12060  sumeq2  12072  summodc  12097  fsum3cvg3  12110  fsum2d  12149  prodeq2  12271  prodmodclem2  12291  fprod2d  12337  eirrap  12492  addmodlteqALT  12573  divalglemeunn  12635  divalglemeuneg  12637  bezoutlemnewy  12720  bezoutlemstep  12721  bezoutlemmain  12722  bezoutlembi  12729  bezoutlemeu  12731  rpdvds  12824  isprm5lem  12866  isprm6  12872  pw2dvdslemn  12890  pw2dvdseu  12893  sqrt2irrap  12905  pythagtriplem2  12992  pythagtrip  13009  pclemub  13013  pcqmul  13029  pcexp  13035  pcneg  13051  pcprmpw2  13059  pcadd  13066  pcmpt  13069  4sqlem13m  13129  ballotfilemcdc  13170  ballotfilemfc0  13179  ballotfilemfcc  13180  ennnfonelemrnh  13254  ennnfonelemnn0  13260  ctinfomlemom  13265  ctiunctlemfo  13277  nninfdclemf1  13290  imasival  13573  gsumpropd2  13659  sgrppropd  13679  ismndd  13701  mndpropd  13704  mhmeql  13750  mhmmnd  13872  issubg4m  13949  ssnmz  13967  conjnmzb  14036  gfsumval  14105  rngpropd  14197  ringpropd  14284  aprlring  14541  islmod  14568  psrval  14943  restbasg  15162  cnrest2  15230  cnpdis  15236  lmtopcnp  15244  txcnp  15265  txlm  15273  ismet2  15348  blininf  15418  metss2lem  15491  xmettxlem  15503  xmettx  15504  metcnp3  15505  metcnpi3  15511  addcncntoplem  15555  fsumcncntop  15561  mulcncf  15602  dedekindeulemuub  15611  dedekindeu  15617  dedekindicclemuub  15620  ivthinclemlopn  15630  ivthinclemuopn  15632  ivthinclemloc  15635  ivthinc  15637  ivthdichlem  15645  limcimo  15659  limccnp2cntop  15671  plyf  15731  plyco  15753  plycj  15755  plyrecj  15757  dvply2g  15760  logbgcd1irrap  15964  perfectlem2  15997  lgsdilem  16029  lgsquad2lem2  16084  lgsquad3  16086  2sqlem5  16121  2sqlem9  16126  usgredg4  16339  usgr1vr  16372  subuhgr  16396  subumgr  16398  clwwlknonex2lem2  16562  eupth2lemsfi  16602  depindlem3  16632  qdencn  16946  apdiff  16971  qdiff  16972  trimul0or  16984