Theorem simplrr 538

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  3125  disjiun  4083  isotr  5957  riota5f  5998  tfrexlem  6500  tfrcl  6530  nnsucuniel  6663  pw2f1odclem  7020  fopwdom  7022  dif1enen  7069  fisbth  7072  fin0  7074  fin0or  7075  diffisn  7082  fidcen  7088  finexdc  7092  elssdc  7094  fientri3  7107  unfidisj  7114  undifdc  7116  ssfirab  7129  fnfi  7135  iunfidisj  7145  dcfi  7180  ordiso2  7234  difinfinf  7300  ctmlemr  7307  exmidfodomrlemr  7413  2omotaplemap  7476  cc2lem  7485  cc3  7487  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  ltexnqq  7628  addcmpblnq0  7663  mulcmpblnq0  7664  prmu  7698  addlocpr  7756  prmuloc  7786  prmuloc2  7787  ltaddpr  7817  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemloc  7827  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  aptiprleml  7859  aptiprlemu  7860  ltmprr  7862  cauappcvgprlemloc  7872  archrecpr  7884  caucvgprlemloc  7895  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  suplocexprlemdisj  7940  suplocexprlemloc  7941  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  ltsrprg  7967  mulgt0sr  7998  caucvgsrlemgt1  8015  suplocsrlemb  8026  axmulcl  8086  axarch  8111  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  readdcan  8319  cnegexlem1  8354  negeu  8370  add20  8654  apreap  8767  cru  8782  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  divdivdivap  8893  ltmul12a  9040  lemul12a  9042  lt2mul2div  9059  ledivdiv  9070  lediv12a  9074  qapne  9873  xleadd1a  10108  ixxss12  10141  ioodisj  10228  fz0fzelfz0  10362  zsupcllemstep  10490  zsupssdc  10499  qtri3or  10501  exbtwnzlemstep  10508  exbtwnzlemex  10510  exbtwnz  10511  rebtwn2zlemstep  10513  rebtwn2z  10515  qbtwnre  10517  btwnzge0  10561  iseqf1olemqf1o  10769  mulexpzap  10842  leexp1a  10857  expnbnd  10926  hashen  11047  fihashdom  11067  hashun  11069  zfz1iso  11106  swrdccat  11317  reuccatpfxs1  11329  cjap  11468  cvg1nlemres  11547  rsqrmo  11589  abs3lem  11673  cau3lem  11676  rexanre  11782  xrmaxltsup  11820  climcau  11909  sumeq2  11921  summodc  11946  fsum3cvg3  11959  fsum2d  11998  prodeq2  12120  prodmodclem2  12140  fprod2d  12186  eirrap  12341  addmodlteqALT  12422  divalglemeunn  12484  divalglemeuneg  12486  bezoutlemnewy  12569  bezoutlemstep  12570  bezoutlemmain  12571  bezoutlembi  12578  bezoutlemeu  12580  rpdvds  12673  isprm5lem  12715  isprm6  12721  pw2dvdslemn  12739  pw2dvdseu  12742  sqrt2irrap  12754  pythagtriplem2  12841  pythagtrip  12858  pclemub  12862  pcqmul  12878  pcexp  12884  pcneg  12900  pcprmpw2  12908  pcadd  12915  pcmpt  12918  4sqlem13m  12978  ennnfonelemrnh  13039  ennnfonelemnn0  13045  ctinfomlemom  13050  ctiunctlemfo  13062  nninfdclemf1  13075  imasival  13391  gsumpropd2  13478  sgrppropd  13498  ismndd  13522  mndpropd  13525  mhmeql  13577  mhmmnd  13705  issubg4m  13782  ssnmz  13800  conjnmzb  13869  rngpropd  13971  ringpropd  14054  islmod  14308  psrval  14683  restbasg  14895  cnrest2  14963  cnpdis  14969  lmtopcnp  14977  txcnp  14998  txlm  15006  ismet2  15081  blininf  15151  metss2lem  15224  xmettxlem  15236  xmettx  15237  metcnp3  15238  metcnpi3  15244  addcncntoplem  15288  fsumcncntop  15294  mulcncf  15335  dedekindeulemuub  15344  dedekindeu  15350  dedekindicclemuub  15353  ivthinclemlopn  15363  ivthinclemuopn  15365  ivthinclemloc  15368  ivthinc  15370  ivthdichlem  15378  limcimo  15392  limccnp2cntop  15404  plyf  15464  plyco  15486  plycj  15488  plyrecj  15490  dvply2g  15493  logbgcd1irrap  15697  perfectlem2  15727  lgsdilem  15759  lgsquad2lem2  15814  lgsquad3  15816  2sqlem5  15851  2sqlem9  15856  usgredg4  16069  usgr1vr  16102  subuhgr  16126  subumgr  16128  clwwlknonex2lem2  16292  eupth2lemsfi  16332  depindlem3  16348  2omap  16615  qdencn  16652  apdiff  16673  gfsumval  16701