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  3070  disjiun  4013  isotr  5834  riota5f  5872  tfrexlem  6354  tfrcl  6384  nnsucuniel  6515  fopwdom  6855  dif1enen  6899  fisbth  6902  fin0  6904  fin0or  6905  diffisn  6912  finexdc  6921  fientri3  6933  unfidisj  6940  undifdc  6942  ssfirab  6952  fnfi  6956  iunfidisj  6965  dcfi  7000  ordiso2  7054  difinfinf  7120  ctmlemr  7127  exmidfodomrlemr  7221  2omotaplemap  7276  cc2lem  7285  cc3  7287  addcmpblnq  7386  mulcmpblnq  7387  ordpipqqs  7393  ltexnqq  7427  addcmpblnq0  7462  mulcmpblnq0  7463  prmu  7497  addlocpr  7555  prmuloc  7585  prmuloc2  7586  ltaddpr  7616  ltexprlemopl  7620  ltexprlemopu  7622  ltexprlemloc  7626  ltexprlemrl  7629  ltexprlemru  7631  addcanprleml  7633  addcanprlemu  7634  aptiprleml  7658  aptiprlemu  7659  ltmprr  7661  cauappcvgprlemloc  7671  archrecpr  7683  caucvgprlemloc  7694  caucvgprprlemloc  7722  caucvgprprlemexbt  7725  suplocexprlemdisj  7739  suplocexprlemloc  7740  addcmpblnr  7758  mulcmpblnrlemg  7759  mulcmpblnr  7760  ltsrprg  7766  mulgt0sr  7797  caucvgsrlemgt1  7814  suplocsrlemb  7825  axmulcl  7885  axarch  7910  axcaucvglemres  7918  axpre-suploclemres  7920  axpre-suploc  7921  readdcan  8117  cnegexlem1  8152  negeu  8168  add20  8451  apreap  8564  cru  8579  apsym  8583  apcotr  8584  apadd1  8585  apneg  8588  mulext1  8589  divdivdivap  8690  ltmul12a  8837  lemul12a  8839  lt2mul2div  8856  ledivdiv  8867  lediv12a  8871  qapne  9659  xleadd1a  9893  ixxss12  9926  ioodisj  10013  fz0fzelfz0  10147  qtri3or  10263  exbtwnzlemstep  10268  exbtwnzlemex  10270  exbtwnz  10271  rebtwn2zlemstep  10273  rebtwn2z  10275  qbtwnre  10277  btwnzge0  10320  iseqf1olemqf1o  10513  mulexpzap  10580  leexp1a  10595  expnbnd  10664  hashen  10784  fihashdom  10803  hashun  10805  zfz1iso  10841  cjap  10935  cvg1nlemres  11014  rsqrmo  11056  abs3lem  11140  cau3lem  11143  rexanre  11249  xrmaxltsup  11286  climcau  11375  sumeq2  11387  summodc  11411  fsum3cvg3  11424  fsum2d  11463  prodeq2  11585  prodmodclem2  11605  fprod2d  11651  eirrap  11805  addmodlteqALT  11885  divalglemeunn  11946  divalglemeuneg  11948  zsupcllemstep  11966  zsupssdc  11975  bezoutlemnewy  12017  bezoutlemstep  12018  bezoutlemmain  12019  bezoutlembi  12026  bezoutlemeu  12028  rpdvds  12119  isprm5lem  12161  isprm6  12167  pw2dvdslemn  12185  pw2dvdseu  12188  sqrt2irrap  12200  pythagtriplem2  12286  pythagtrip  12303  pclemub  12307  pcqmul  12323  pcexp  12329  pcneg  12344  pcprmpw2  12352  pcadd  12359  pcmpt  12361  ennnfonelemrnh  12442  ennnfonelemnn0  12448  ctinfomlemom  12453  ctiunctlemfo  12465  nninfdclemf1  12478  imasival  12756  sgrppropd  12849  ismndd  12871  mndpropd  12874  mhmeql  12917  mhmmnd  13031  issubg4m  13105  ssnmz  13123  conjnmzb  13187  rngpropd  13277  ringpropd  13360  islmod  13575  restbasg  14072  cnrest2  14140  cnpdis  14146  lmtopcnp  14154  txcnp  14175  txlm  14183  ismet2  14258  blininf  14328  metss2lem  14401  xmettxlem  14413  xmettx  14414  metcnp3  14415  metcnpi3  14421  addcncntoplem  14455  fsumcncntop  14460  mulcncf  14495  dedekindeulemuub  14499  dedekindeu  14505  dedekindicclemuub  14508  ivthinclemlopn  14518  ivthinclemuopn  14520  ivthinclemloc  14523  ivthinc  14525  limcimo  14538  limccnp2cntop  14550  logbgcd1irrap  14792  lgsdilem  14832  2sqlem5  14870  2sqlem9  14875  qdencn  15180  apdiff  15201