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  3122  disjiun  4078  isotr  5949  riota5f  5990  tfrexlem  6491  tfrcl  6521  nnsucuniel  6654  pw2f1odclem  7008  fopwdom  7010  dif1enen  7055  fisbth  7058  fin0  7060  fin0or  7061  diffisn  7068  fidcen  7074  finexdc  7078  elssdc  7080  fientri3  7093  unfidisj  7100  undifdc  7102  ssfirab  7114  fnfi  7119  iunfidisj  7129  dcfi  7164  ordiso2  7218  difinfinf  7284  ctmlemr  7291  exmidfodomrlemr  7396  2omotaplemap  7459  cc2lem  7468  cc3  7470  addcmpblnq  7570  mulcmpblnq  7571  ordpipqqs  7577  ltexnqq  7611  addcmpblnq0  7646  mulcmpblnq0  7647  prmu  7681  addlocpr  7739  prmuloc  7769  prmuloc2  7770  ltaddpr  7800  ltexprlemopl  7804  ltexprlemopu  7806  ltexprlemloc  7810  ltexprlemrl  7813  ltexprlemru  7815  addcanprleml  7817  addcanprlemu  7818  aptiprleml  7842  aptiprlemu  7843  ltmprr  7845  cauappcvgprlemloc  7855  archrecpr  7867  caucvgprlemloc  7878  caucvgprprlemloc  7906  caucvgprprlemexbt  7909  suplocexprlemdisj  7923  suplocexprlemloc  7924  addcmpblnr  7942  mulcmpblnrlemg  7943  mulcmpblnr  7944  ltsrprg  7950  mulgt0sr  7981  caucvgsrlemgt1  7998  suplocsrlemb  8009  axmulcl  8069  axarch  8094  axcaucvglemres  8102  axpre-suploclemres  8104  axpre-suploc  8105  readdcan  8302  cnegexlem1  8337  negeu  8353  add20  8637  apreap  8750  cru  8765  apsym  8769  apcotr  8770  apadd1  8771  apneg  8774  mulext1  8775  divdivdivap  8876  ltmul12a  9023  lemul12a  9025  lt2mul2div  9042  ledivdiv  9053  lediv12a  9057  qapne  9851  xleadd1a  10086  ixxss12  10119  ioodisj  10206  fz0fzelfz0  10340  zsupcllemstep  10466  zsupssdc  10475  qtri3or  10477  exbtwnzlemstep  10484  exbtwnzlemex  10486  exbtwnz  10487  rebtwn2zlemstep  10489  rebtwn2z  10491  qbtwnre  10493  btwnzge0  10537  iseqf1olemqf1o  10745  mulexpzap  10818  leexp1a  10833  expnbnd  10902  hashen  11023  fihashdom  11042  hashun  11044  zfz1iso  11081  swrdccat  11288  reuccatpfxs1  11300  cjap  11438  cvg1nlemres  11517  rsqrmo  11559  abs3lem  11643  cau3lem  11646  rexanre  11752  xrmaxltsup  11790  climcau  11879  sumeq2  11891  summodc  11915  fsum3cvg3  11928  fsum2d  11967  prodeq2  12089  prodmodclem2  12109  fprod2d  12155  eirrap  12310  addmodlteqALT  12391  divalglemeunn  12453  divalglemeuneg  12455  bezoutlemnewy  12538  bezoutlemstep  12539  bezoutlemmain  12540  bezoutlembi  12547  bezoutlemeu  12549  rpdvds  12642  isprm5lem  12684  isprm6  12690  pw2dvdslemn  12708  pw2dvdseu  12711  sqrt2irrap  12723  pythagtriplem2  12810  pythagtrip  12827  pclemub  12831  pcqmul  12847  pcexp  12853  pcneg  12869  pcprmpw2  12877  pcadd  12884  pcmpt  12887  4sqlem13m  12947  ennnfonelemrnh  13008  ennnfonelemnn0  13014  ctinfomlemom  13019  ctiunctlemfo  13031  nninfdclemf1  13044  imasival  13360  gsumpropd2  13447  sgrppropd  13467  ismndd  13491  mndpropd  13494  mhmeql  13546  mhmmnd  13674  issubg4m  13751  ssnmz  13769  conjnmzb  13838  rngpropd  13939  ringpropd  14022  islmod  14276  psrval  14651  restbasg  14863  cnrest2  14931  cnpdis  14937  lmtopcnp  14945  txcnp  14966  txlm  14974  ismet2  15049  blininf  15119  metss2lem  15192  xmettxlem  15204  xmettx  15205  metcnp3  15206  metcnpi3  15212  addcncntoplem  15256  fsumcncntop  15262  mulcncf  15303  dedekindeulemuub  15312  dedekindeu  15318  dedekindicclemuub  15321  ivthinclemlopn  15331  ivthinclemuopn  15333  ivthinclemloc  15336  ivthinc  15338  ivthdichlem  15346  limcimo  15360  limccnp2cntop  15372  plyf  15432  plyco  15454  plycj  15456  plyrecj  15458  dvply2g  15461  logbgcd1irrap  15665  perfectlem2  15695  lgsdilem  15727  lgsquad2lem2  15782  lgsquad3  15784  2sqlem5  15819  2sqlem9  15824  usgredg4  16034  usgr1vr  16067  2omap  16472  qdencn  16509  apdiff  16530