Theorem simp2r 1050

Description: Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)

Assertion

Ref	Expression
simp2r	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simp2r

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant2 1045	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1004

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 depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  simpl2r  1077  simpr2r  1083  simp12r  1137  simp22r  1143  simp32r  1149  issod  4416  funprg  5380  fsnunf  5854  f1oiso2  5968  tfrlemibxssdm  6493  ecopovtrn  6801  ecopovtrng  6804  dftap2  7470  addassnqg  7602  ltsonq  7618  ltanqg  7620  ltmnqg  7621  addassnq0  7682  recexprlem1ssl  7853  mulasssrg  7978  distrsrg  7979  lttrsr  7982  ltsosr  7984  ltasrg  7990  mulextsr1lem  8000  mulextsr1  8001  axmulass  8093  axdistr  8094  dmdcanap  8902  lediv2  9071  ltdiv23  9072  lediv23  9073  xaddass2  10105  xlt2add  10115  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  expdivap  10853  leisorel  11102  swrdspsleq  11252  pfxeq  11281  ccatopth2  11302  bdtrilem  11804  xrbdtri  11841  fldivndvdslt  12503  prmexpb  12728  pcpremul  12871  pcdiv  12880  pcqmul  12881  pcqdiv  12885  4sqlem12  12980  f1ocpbllem  13398  ercpbl  13419  erlecpbl  13420  cmn4  13897  ablsub4  13905  abladdsub4  13906  cnptoprest  14969  ssblps  15155  ssbl  15156  tgqioo  15285  plyadd  15481  plymul  15482  rplogbchbase  15680