Theorem simplrr 508

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 109	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antlr 478	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  rmob  2967  disjiun  3888  isotr  5669  riota5f  5706  tfrexlem  6182  tfrcl  6212  nnsucuniel  6342  fopwdom  6680  dif1enen  6724  fisbth  6727  fin0  6729  fin0or  6730  diffisn  6737  finexdc  6746  fientri3  6753  unfidisj  6760  undifdc  6762  ssfirab  6771  fnfi  6774  iunfidisj  6783  ordiso2  6869  difinfinf  6935  ctmlemr  6942  exmidfodomrlemr  7002  addcmpblnq  7116  mulcmpblnq  7117  ordpipqqs  7123  ltexnqq  7157  addcmpblnq0  7192  mulcmpblnq0  7193  prmu  7227  addlocpr  7285  prmuloc  7315  prmuloc2  7316  ltaddpr  7346  ltexprlemopl  7350  ltexprlemopu  7352  ltexprlemloc  7356  ltexprlemrl  7359  ltexprlemru  7361  addcanprleml  7363  addcanprlemu  7364  aptiprleml  7388  aptiprlemu  7389  ltmprr  7391  cauappcvgprlemloc  7401  archrecpr  7413  caucvgprlemloc  7424  caucvgprprlemloc  7452  caucvgprprlemexbt  7455  addcmpblnr  7475  mulcmpblnrlemg  7476  mulcmpblnr  7477  ltsrprg  7483  mulgt0sr  7513  caucvgsrlemgt1  7530  axmulcl  7594  axarch  7619  axcaucvglemres  7627  readdcan  7818  cnegexlem1  7853  negeu  7869  add20  8148  apreap  8260  cru  8275  apsym  8279  apcotr  8280  apadd1  8281  apneg  8284  mulext1  8285  divdivdivap  8379  ltmul12a  8521  lemul12a  8523  lt2mul2div  8540  ledivdiv  8551  lediv12a  8555  qapne  9326  xleadd1a  9542  ixxss12  9575  ioodisj  9662  fz0fzelfz0  9790  qtri3or  9906  exbtwnzlemstep  9911  exbtwnzlemex  9913  exbtwnz  9914  rebtwn2zlemstep  9916  rebtwn2z  9918  qbtwnre  9920  btwnzge0  9959  iseqf1olemqf1o  10152  mulexpzap  10219  leexp1a  10234  expnbnd  10301  hashen  10416  fihashdom  10435  hashun  10437  zfz1iso  10470  cjap  10564  cvg1nlemres  10642  rsqrmo  10684  abs3lem  10768  cau3lem  10771  rexanre  10877  xrmaxltsup  10912  climcau  11001  sumeq2  11013  summodc  11037  fsum3cvg3  11050  fsum2d  11089  eirrap  11325  addmodlteqALT  11398  divalglemeunn  11459  divalglemeuneg  11461  zsupcllemstep  11479  bezoutlemnewy  11523  bezoutlemstep  11524  bezoutlemmain  11525  bezoutlembi  11532  bezoutlemeu  11534  rpdvds  11619  isprm6  11664  pw2dvdslemn  11681  pw2dvdseu  11684  sqrt2irrap  11696  ennnfonelemrnh  11767  ennnfonelemnn0  11773  ctinfomlemom  11778  ctiunctlemfo  11788  restbasg  12173  cnrest2  12240  cnpdis  12246  lmtopcnp  12254  txcnp  12275  txlm  12283  ismet2  12336  blininf  12406  metss2lem  12479  xmettxlem  12491  xmettx  12492  metcnp3  12493  metcnpi3  12499  addcncntoplem  12530  fsumcncntop  12535  mulcncf  12570  limcimo  12583  limccnp2cntop  12595  qdencn  12899