Theorem simp2r 940

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

Syntax hints:   → wi 4   ∧ wa 101   ∧ w3a 894

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

This theorem depends on definitions:  df-bi 114  df-3an 896

This theorem is referenced by:  simpl2r  967  simpr2r  973  simp12r  1027  simp22r  1033  simp32r  1039  issod  4081  funprg  4974  fsnunf  5387  f1oiso2  5491  tfrlemibxssdm  5969  ecopovtrn  6231  ecopovtrng  6234  addassnqg  6508  ltsonq  6524  ltanqg  6526  ltmnqg  6527  addassnq0  6588  recexprlem1ssl  6759  mulasssrg  6871  distrsrg  6872  lttrsr  6875  ltsosr  6877  ltasrg  6883  mulextsr1lem  6892  mulextsr1  6893  axmulass  6975  axdistr  6976  dmdcanap  7743  lediv2  7902  ltdiv23  7903  lediv23  7904  expaddzaplem  9428  expaddzap  9429  expmulzap  9431  expdivap  9436