Theorem simp2r 1014

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 968

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

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  simpl2r  1041  simpr2r  1047  simp12r  1101  simp22r  1107  simp32r  1113  issod  4297  funprg  5238  fsnunf  5685  f1oiso2  5795  tfrlemibxssdm  6295  ecopovtrn  6598  ecopovtrng  6601  addassnqg  7323  ltsonq  7339  ltanqg  7341  ltmnqg  7342  addassnq0  7403  recexprlem1ssl  7574  mulasssrg  7699  distrsrg  7700  lttrsr  7703  ltsosr  7705  ltasrg  7711  mulextsr1lem  7721  mulextsr1  7722  axmulass  7814  axdistr  7815  dmdcanap  8618  lediv2  8786  ltdiv23  8787  lediv23  8788  xaddass2  9806  xlt2add  9816  expaddzaplem  10498  expaddzap  10499  expmulzap  10501  expdivap  10506  leisorel  10750  bdtrilem  11180  xrbdtri  11217  fldivndvdslt  11872  prmexpb  12083  pcpremul  12225  pcdiv  12234  pcqmul  12235  pcqdiv  12239  cnptoprest  12879  ssblps  13065  ssbl  13066  tgqioo  13187  rplogbchbase  13508