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  3056  disjiun  3999  isotr  5817  riota5f  5855  tfrexlem  6335  tfrcl  6365  nnsucuniel  6496  fopwdom  6836  dif1enen  6880  fisbth  6883  fin0  6885  fin0or  6886  diffisn  6893  finexdc  6902  fientri3  6914  unfidisj  6921  undifdc  6923  ssfirab  6933  fnfi  6936  iunfidisj  6945  dcfi  6980  ordiso2  7034  difinfinf  7100  ctmlemr  7107  exmidfodomrlemr  7201  2omotaplemap  7256  cc2lem  7265  cc3  7267  addcmpblnq  7366  mulcmpblnq  7367  ordpipqqs  7373  ltexnqq  7407  addcmpblnq0  7442  mulcmpblnq0  7443  prmu  7477  addlocpr  7535  prmuloc  7565  prmuloc2  7566  ltaddpr  7596  ltexprlemopl  7600  ltexprlemopu  7602  ltexprlemloc  7606  ltexprlemrl  7609  ltexprlemru  7611  addcanprleml  7613  addcanprlemu  7614  aptiprleml  7638  aptiprlemu  7639  ltmprr  7641  cauappcvgprlemloc  7651  archrecpr  7663  caucvgprlemloc  7674  caucvgprprlemloc  7702  caucvgprprlemexbt  7705  suplocexprlemdisj  7719  suplocexprlemloc  7720  addcmpblnr  7738  mulcmpblnrlemg  7739  mulcmpblnr  7740  ltsrprg  7746  mulgt0sr  7777  caucvgsrlemgt1  7794  suplocsrlemb  7805  axmulcl  7865  axarch  7890  axcaucvglemres  7898  axpre-suploclemres  7900  axpre-suploc  7901  readdcan  8097  cnegexlem1  8132  negeu  8148  add20  8431  apreap  8544  cru  8559  apsym  8563  apcotr  8564  apadd1  8565  apneg  8568  mulext1  8569  divdivdivap  8670  ltmul12a  8817  lemul12a  8819  lt2mul2div  8836  ledivdiv  8847  lediv12a  8851  qapne  9639  xleadd1a  9873  ixxss12  9906  ioodisj  9993  fz0fzelfz0  10127  qtri3or  10243  exbtwnzlemstep  10248  exbtwnzlemex  10250  exbtwnz  10251  rebtwn2zlemstep  10253  rebtwn2z  10255  qbtwnre  10257  btwnzge0  10300  iseqf1olemqf1o  10493  mulexpzap  10560  leexp1a  10575  expnbnd  10644  hashen  10764  fihashdom  10783  hashun  10785  zfz1iso  10821  cjap  10915  cvg1nlemres  10994  rsqrmo  11036  abs3lem  11120  cau3lem  11123  rexanre  11229  xrmaxltsup  11266  climcau  11355  sumeq2  11367  summodc  11391  fsum3cvg3  11404  fsum2d  11443  prodeq2  11565  prodmodclem2  11585  fprod2d  11631  eirrap  11785  addmodlteqALT  11865  divalglemeunn  11926  divalglemeuneg  11928  zsupcllemstep  11946  zsupssdc  11955  bezoutlemnewy  11997  bezoutlemstep  11998  bezoutlemmain  11999  bezoutlembi  12006  bezoutlemeu  12008  rpdvds  12099  isprm5lem  12141  isprm6  12147  pw2dvdslemn  12165  pw2dvdseu  12168  sqrt2irrap  12180  pythagtriplem2  12266  pythagtrip  12283  pclemub  12287  pcqmul  12303  pcexp  12309  pcneg  12324  pcprmpw2  12332  pcadd  12339  pcmpt  12341  ennnfonelemrnh  12417  ennnfonelemnn0  12423  ctinfomlemom  12428  ctiunctlemfo  12440  nninfdclemf1  12453  imasival  12727  ismndd  12838  mndpropd  12841  mhmeql  12876  mhmmnd  12980  issubg4m  13053  ssnmz  13071  ringpropd  13217  islmod  13381  restbasg  13671  cnrest2  13739  cnpdis  13745  lmtopcnp  13753  txcnp  13774  txlm  13782  ismet2  13857  blininf  13927  metss2lem  14000  xmettxlem  14012  xmettx  14013  metcnp3  14014  metcnpi3  14020  addcncntoplem  14054  fsumcncntop  14059  mulcncf  14094  dedekindeulemuub  14098  dedekindeu  14104  dedekindicclemuub  14107  ivthinclemlopn  14117  ivthinclemuopn  14119  ivthinclemloc  14122  ivthinc  14124  limcimo  14137  limccnp2cntop  14149  logbgcd1irrap  14391  lgsdilem  14431  2sqlem5  14469  2sqlem9  14474  qdencn  14778  apdiff  14799