Theorem simp2l 967

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

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

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 924

This theorem is referenced by:  simpl2l  994  simpr2l  1000  simp12l  1054  simp22l  1060  simp32l  1066  issod  4120  funprg  5029  fsnunf  5459  f1oiso2  5567  ecopovtrn  6341  ecopovtrng  6344  addassnqg  6885  ltsonq  6901  ltanqg  6903  ltmnqg  6904  addassnq0  6965  recexprlem1ssu  7137  mulasssrg  7248  distrsrg  7249  lttrsr  7252  ltsosr  7254  ltasrg  7260  mulextsr1lem  7269  mulextsr1  7270  axmulass  7352  axdistr  7353  dmdcanap  8128  ltdiv2  8283  lediv2  8287  ltdiv23  8288  lediv23  8289  expaddzaplem  9897  expaddzap  9898  expmulzap  9900  expdivap  9905  leisorel  10139  prmexpb  11012