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  3102  disjiun  4057  isotr  5913  riota5f  5954  tfrexlem  6450  tfrcl  6480  nnsucuniel  6611  pw2f1odclem  6963  fopwdom  6965  dif1enen  7010  fisbth  7013  fin0  7015  fin0or  7016  diffisn  7023  finexdc  7032  fientri3  7045  unfidisj  7052  undifdc  7054  ssfirab  7066  fnfi  7071  iunfidisj  7081  dcfi  7116  ordiso2  7170  difinfinf  7236  ctmlemr  7243  exmidfodomrlemr  7348  2omotaplemap  7411  cc2lem  7420  cc3  7422  addcmpblnq  7522  mulcmpblnq  7523  ordpipqqs  7529  ltexnqq  7563  addcmpblnq0  7598  mulcmpblnq0  7599  prmu  7633  addlocpr  7691  prmuloc  7721  prmuloc2  7722  ltaddpr  7752  ltexprlemopl  7756  ltexprlemopu  7758  ltexprlemloc  7762  ltexprlemrl  7765  ltexprlemru  7767  addcanprleml  7769  addcanprlemu  7770  aptiprleml  7794  aptiprlemu  7795  ltmprr  7797  cauappcvgprlemloc  7807  archrecpr  7819  caucvgprlemloc  7830  caucvgprprlemloc  7858  caucvgprprlemexbt  7861  suplocexprlemdisj  7875  suplocexprlemloc  7876  addcmpblnr  7894  mulcmpblnrlemg  7895  mulcmpblnr  7896  ltsrprg  7902  mulgt0sr  7933  caucvgsrlemgt1  7950  suplocsrlemb  7961  axmulcl  8021  axarch  8046  axcaucvglemres  8054  axpre-suploclemres  8056  axpre-suploc  8057  readdcan  8254  cnegexlem1  8289  negeu  8305  add20  8589  apreap  8702  cru  8717  apsym  8721  apcotr  8722  apadd1  8723  apneg  8726  mulext1  8727  divdivdivap  8828  ltmul12a  8975  lemul12a  8977  lt2mul2div  8994  ledivdiv  9005  lediv12a  9009  qapne  9802  xleadd1a  10037  ixxss12  10070  ioodisj  10157  fz0fzelfz0  10291  zsupcllemstep  10416  zsupssdc  10425  qtri3or  10427  exbtwnzlemstep  10434  exbtwnzlemex  10436  exbtwnz  10437  rebtwn2zlemstep  10439  rebtwn2z  10441  qbtwnre  10443  btwnzge0  10487  iseqf1olemqf1o  10695  mulexpzap  10768  leexp1a  10783  expnbnd  10852  hashen  10973  fihashdom  10992  hashun  10994  zfz1iso  11030  swrdccat  11233  reuccatpfxs1  11245  cjap  11383  cvg1nlemres  11462  rsqrmo  11504  abs3lem  11588  cau3lem  11591  rexanre  11697  xrmaxltsup  11735  climcau  11824  sumeq2  11836  summodc  11860  fsum3cvg3  11873  fsum2d  11912  prodeq2  12034  prodmodclem2  12054  fprod2d  12100  eirrap  12255  addmodlteqALT  12336  divalglemeunn  12398  divalglemeuneg  12400  bezoutlemnewy  12483  bezoutlemstep  12484  bezoutlemmain  12485  bezoutlembi  12492  bezoutlemeu  12494  rpdvds  12587  isprm5lem  12629  isprm6  12635  pw2dvdslemn  12653  pw2dvdseu  12656  sqrt2irrap  12668  pythagtriplem2  12755  pythagtrip  12772  pclemub  12776  pcqmul  12792  pcexp  12798  pcneg  12814  pcprmpw2  12822  pcadd  12829  pcmpt  12832  4sqlem13m  12892  ennnfonelemrnh  12953  ennnfonelemnn0  12959  ctinfomlemom  12964  ctiunctlemfo  12976  nninfdclemf1  12989  imasival  13305  gsumpropd2  13392  sgrppropd  13412  ismndd  13436  mndpropd  13439  mhmeql  13491  mhmmnd  13619  issubg4m  13696  ssnmz  13714  conjnmzb  13783  rngpropd  13884  ringpropd  13967  islmod  14220  psrval  14595  restbasg  14807  cnrest2  14875  cnpdis  14881  lmtopcnp  14889  txcnp  14910  txlm  14918  ismet2  14993  blininf  15063  metss2lem  15136  xmettxlem  15148  xmettx  15149  metcnp3  15150  metcnpi3  15156  addcncntoplem  15200  fsumcncntop  15206  mulcncf  15247  dedekindeulemuub  15256  dedekindeu  15262  dedekindicclemuub  15265  ivthinclemlopn  15275  ivthinclemuopn  15277  ivthinclemloc  15280  ivthinc  15282  ivthdichlem  15290  limcimo  15304  limccnp2cntop  15316  plyf  15376  plyco  15398  plycj  15400  plyrecj  15402  dvply2g  15405  logbgcd1irrap  15609  perfectlem2  15639  lgsdilem  15671  lgsquad2lem2  15726  lgsquad3  15728  2sqlem5  15763  2sqlem9  15768  usgredg4  15978  2omap  16270  qdencn  16306  apdiff  16327