Theorem simp2l 939

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

Assertion

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

Proof of Theorem simp2l

Step	Hyp	Ref	Expression
1		simpl 106	. 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:  simpl2l  966  simpr2l  972  simp12l  1026  simp22l  1032  simp32l  1038  issod  4081  funprg  4974  fsnunf  5387  f1oiso2  5491  ecopovtrn  6231  ecopovtrng  6234  addassnqg  6508  ltsonq  6524  ltanqg  6526  ltmnqg  6527  addassnq0  6588  recexprlem1ssu  6760  mulasssrg  6871  distrsrg  6872  lttrsr  6875  ltsosr  6877  ltasrg  6883  mulextsr1lem  6892  mulextsr1  6893  axmulass  6975  axdistr  6976  dmdcanap  7743  ltdiv2  7898  lediv2  7902  ltdiv23  7903  lediv23  7904  expaddzaplem  9428  expaddzap  9429  expmulzap  9431  expdivap  9436