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  3082  disjiun  4028  isotr  5863  riota5f  5902  tfrexlem  6392  tfrcl  6422  nnsucuniel  6553  pw2f1odclem  6895  fopwdom  6897  dif1enen  6941  fisbth  6944  fin0  6946  fin0or  6947  diffisn  6954  finexdc  6963  fientri3  6976  unfidisj  6983  undifdc  6985  ssfirab  6997  fnfi  7002  iunfidisj  7012  dcfi  7047  ordiso2  7101  difinfinf  7167  ctmlemr  7174  exmidfodomrlemr  7269  2omotaplemap  7324  cc2lem  7333  cc3  7335  addcmpblnq  7434  mulcmpblnq  7435  ordpipqqs  7441  ltexnqq  7475  addcmpblnq0  7510  mulcmpblnq0  7511  prmu  7545  addlocpr  7603  prmuloc  7633  prmuloc2  7634  ltaddpr  7664  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemloc  7674  ltexprlemrl  7677  ltexprlemru  7679  addcanprleml  7681  addcanprlemu  7682  aptiprleml  7706  aptiprlemu  7707  ltmprr  7709  cauappcvgprlemloc  7719  archrecpr  7731  caucvgprlemloc  7742  caucvgprprlemloc  7770  caucvgprprlemexbt  7773  suplocexprlemdisj  7787  suplocexprlemloc  7788  addcmpblnr  7806  mulcmpblnrlemg  7807  mulcmpblnr  7808  ltsrprg  7814  mulgt0sr  7845  caucvgsrlemgt1  7862  suplocsrlemb  7873  axmulcl  7933  axarch  7958  axcaucvglemres  7966  axpre-suploclemres  7968  axpre-suploc  7969  readdcan  8166  cnegexlem1  8201  negeu  8217  add20  8501  apreap  8614  cru  8629  apsym  8633  apcotr  8634  apadd1  8635  apneg  8638  mulext1  8639  divdivdivap  8740  ltmul12a  8887  lemul12a  8889  lt2mul2div  8906  ledivdiv  8917  lediv12a  8921  qapne  9713  xleadd1a  9948  ixxss12  9981  ioodisj  10068  fz0fzelfz0  10202  zsupcllemstep  10319  zsupssdc  10328  qtri3or  10330  exbtwnzlemstep  10337  exbtwnzlemex  10339  exbtwnz  10340  rebtwn2zlemstep  10342  rebtwn2z  10344  qbtwnre  10346  btwnzge0  10390  iseqf1olemqf1o  10598  mulexpzap  10671  leexp1a  10686  expnbnd  10755  hashen  10876  fihashdom  10895  hashun  10897  zfz1iso  10933  cjap  11071  cvg1nlemres  11150  rsqrmo  11192  abs3lem  11276  cau3lem  11279  rexanre  11385  xrmaxltsup  11423  climcau  11512  sumeq2  11524  summodc  11548  fsum3cvg3  11561  fsum2d  11600  prodeq2  11722  prodmodclem2  11742  fprod2d  11788  eirrap  11943  addmodlteqALT  12024  divalglemeunn  12086  divalglemeuneg  12088  bezoutlemnewy  12163  bezoutlemstep  12164  bezoutlemmain  12165  bezoutlembi  12172  bezoutlemeu  12174  rpdvds  12267  isprm5lem  12309  isprm6  12315  pw2dvdslemn  12333  pw2dvdseu  12336  sqrt2irrap  12348  pythagtriplem2  12435  pythagtrip  12452  pclemub  12456  pcqmul  12472  pcexp  12478  pcneg  12494  pcprmpw2  12502  pcadd  12509  pcmpt  12512  4sqlem13m  12572  ennnfonelemrnh  12633  ennnfonelemnn0  12639  ctinfomlemom  12644  ctiunctlemfo  12656  nninfdclemf1  12669  imasival  12949  gsumpropd2  13036  sgrppropd  13056  ismndd  13078  mndpropd  13081  mhmeql  13124  mhmmnd  13246  issubg4m  13323  ssnmz  13341  conjnmzb  13410  rngpropd  13511  ringpropd  13594  islmod  13847  psrval  14220  restbasg  14404  cnrest2  14472  cnpdis  14478  lmtopcnp  14486  txcnp  14507  txlm  14515  ismet2  14590  blininf  14660  metss2lem  14733  xmettxlem  14745  xmettx  14746  metcnp3  14747  metcnpi3  14753  addcncntoplem  14797  fsumcncntop  14803  mulcncf  14844  dedekindeulemuub  14853  dedekindeu  14859  dedekindicclemuub  14862  ivthinclemlopn  14872  ivthinclemuopn  14874  ivthinclemloc  14877  ivthinc  14879  ivthdichlem  14887  limcimo  14901  limccnp2cntop  14913  plyf  14973  plyco  14995  plycj  14997  plyrecj  14999  dvply2g  15002  logbgcd1irrap  15206  perfectlem2  15236  lgsdilem  15268  lgsquad2lem2  15323  lgsquad3  15325  2sqlem5  15360  2sqlem9  15365  qdencn  15671  apdiff  15692