Theorem simp2r 1048

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 1043	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

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

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 1004

This theorem is referenced by:  simpl2r  1075  simpr2r  1081  simp12r  1135  simp22r  1141  simp32r  1147  issod  4407  funprg  5367  fsnunf  5832  f1oiso2  5944  tfrlemibxssdm  6463  ecopovtrn  6769  ecopovtrng  6772  dftap2  7425  addassnqg  7557  ltsonq  7573  ltanqg  7575  ltmnqg  7576  addassnq0  7637  recexprlem1ssl  7808  mulasssrg  7933  distrsrg  7934  lttrsr  7937  ltsosr  7939  ltasrg  7945  mulextsr1lem  7955  mulextsr1  7956  axmulass  8048  axdistr  8049  dmdcanap  8857  lediv2  9026  ltdiv23  9027  lediv23  9028  xaddass2  10054  xlt2add  10064  expaddzaplem  10791  expaddzap  10792  expmulzap  10794  expdivap  10799  leisorel  11046  swrdspsleq  11185  pfxeq  11214  ccatopth2  11235  bdtrilem  11736  xrbdtri  11773  fldivndvdslt  12434  prmexpb  12659  pcpremul  12802  pcdiv  12811  pcqmul  12812  pcqdiv  12816  4sqlem12  12911  f1ocpbllem  13329  ercpbl  13350  erlecpbl  13351  cmn4  13828  ablsub4  13836  abladdsub4  13837  cnptoprest  14898  ssblps  15084  ssbl  15085  tgqioo  15214  plyadd  15410  plymul  15411  rplogbchbase  15609