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  3092  disjiun  4042  isotr  5892  riota5f  5931  tfrexlem  6427  tfrcl  6457  nnsucuniel  6588  pw2f1odclem  6938  fopwdom  6940  dif1enen  6984  fisbth  6987  fin0  6989  fin0or  6990  diffisn  6997  finexdc  7006  fientri3  7019  unfidisj  7026  undifdc  7028  ssfirab  7040  fnfi  7045  iunfidisj  7055  dcfi  7090  ordiso2  7144  difinfinf  7210  ctmlemr  7217  exmidfodomrlemr  7317  2omotaplemap  7376  cc2lem  7385  cc3  7387  addcmpblnq  7487  mulcmpblnq  7488  ordpipqqs  7494  ltexnqq  7528  addcmpblnq0  7563  mulcmpblnq0  7564  prmu  7598  addlocpr  7656  prmuloc  7686  prmuloc2  7687  ltaddpr  7717  ltexprlemopl  7721  ltexprlemopu  7723  ltexprlemloc  7727  ltexprlemrl  7730  ltexprlemru  7732  addcanprleml  7734  addcanprlemu  7735  aptiprleml  7759  aptiprlemu  7760  ltmprr  7762  cauappcvgprlemloc  7772  archrecpr  7784  caucvgprlemloc  7795  caucvgprprlemloc  7823  caucvgprprlemexbt  7826  suplocexprlemdisj  7840  suplocexprlemloc  7841  addcmpblnr  7859  mulcmpblnrlemg  7860  mulcmpblnr  7861  ltsrprg  7867  mulgt0sr  7898  caucvgsrlemgt1  7915  suplocsrlemb  7926  axmulcl  7986  axarch  8011  axcaucvglemres  8019  axpre-suploclemres  8021  axpre-suploc  8022  readdcan  8219  cnegexlem1  8254  negeu  8270  add20  8554  apreap  8667  cru  8682  apsym  8686  apcotr  8687  apadd1  8688  apneg  8691  mulext1  8692  divdivdivap  8793  ltmul12a  8940  lemul12a  8942  lt2mul2div  8959  ledivdiv  8970  lediv12a  8974  qapne  9767  xleadd1a  10002  ixxss12  10035  ioodisj  10122  fz0fzelfz0  10256  zsupcllemstep  10379  zsupssdc  10388  qtri3or  10390  exbtwnzlemstep  10397  exbtwnzlemex  10399  exbtwnz  10400  rebtwn2zlemstep  10402  rebtwn2z  10404  qbtwnre  10406  btwnzge0  10450  iseqf1olemqf1o  10658  mulexpzap  10731  leexp1a  10746  expnbnd  10815  hashen  10936  fihashdom  10955  hashun  10957  zfz1iso  10993  cjap  11261  cvg1nlemres  11340  rsqrmo  11382  abs3lem  11466  cau3lem  11469  rexanre  11575  xrmaxltsup  11613  climcau  11702  sumeq2  11714  summodc  11738  fsum3cvg3  11751  fsum2d  11790  prodeq2  11912  prodmodclem2  11932  fprod2d  11978  eirrap  12133  addmodlteqALT  12214  divalglemeunn  12276  divalglemeuneg  12278  bezoutlemnewy  12361  bezoutlemstep  12362  bezoutlemmain  12363  bezoutlembi  12370  bezoutlemeu  12372  rpdvds  12465  isprm5lem  12507  isprm6  12513  pw2dvdslemn  12531  pw2dvdseu  12534  sqrt2irrap  12546  pythagtriplem2  12633  pythagtrip  12650  pclemub  12654  pcqmul  12670  pcexp  12676  pcneg  12692  pcprmpw2  12700  pcadd  12707  pcmpt  12710  4sqlem13m  12770  ennnfonelemrnh  12831  ennnfonelemnn0  12837  ctinfomlemom  12842  ctiunctlemfo  12854  nninfdclemf1  12867  imasival  13182  gsumpropd2  13269  sgrppropd  13289  ismndd  13313  mndpropd  13316  mhmeql  13368  mhmmnd  13496  issubg4m  13573  ssnmz  13591  conjnmzb  13660  rngpropd  13761  ringpropd  13844  islmod  14097  psrval  14472  restbasg  14684  cnrest2  14752  cnpdis  14758  lmtopcnp  14766  txcnp  14787  txlm  14795  ismet2  14870  blininf  14940  metss2lem  15013  xmettxlem  15025  xmettx  15026  metcnp3  15027  metcnpi3  15033  addcncntoplem  15077  fsumcncntop  15083  mulcncf  15124  dedekindeulemuub  15133  dedekindeu  15139  dedekindicclemuub  15142  ivthinclemlopn  15152  ivthinclemuopn  15154  ivthinclemloc  15157  ivthinc  15159  ivthdichlem  15167  limcimo  15181  limccnp2cntop  15193  plyf  15253  plyco  15275  plycj  15277  plyrecj  15279  dvply2g  15282  logbgcd1irrap  15486  perfectlem2  15516  lgsdilem  15548  lgsquad2lem2  15603  lgsquad3  15605  2sqlem5  15640  2sqlem9  15645  2omap  16006  qdencn  16040  apdiff  16061