Theorem simp2r 965

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

Syntax hints:   → wi 4   ∧ wa 102   ∧ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simpl2r  992  simpr2r  998  simp12r  1052  simp22r  1058  simp32r  1064  issod  4074  funprg  4969  fsnunf  5383  f1oiso2  5486  tfrlemibxssdm  5964  ecopovtrn  6226  ecopovtrng  6229  addassnqg  6572  ltsonq  6588  ltanqg  6590  ltmnqg  6591  addassnq0  6652  recexprlem1ssl  6823  mulasssrg  6935  distrsrg  6936  lttrsr  6939  ltsosr  6941  ltasrg  6947  mulextsr1lem  6956  mulextsr1  6957  axmulass  7039  axdistr  7040  dmdcanap  7810  lediv2  7969  ltdiv23  7970  lediv23  7971  expaddzaplem  9519  expaddzap  9520  expmulzap  9522  expdivap  9527  fldivndvdslt  10335  prmexpb  10530