Theorem simp2l 965

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 961	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

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

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 922

This theorem is referenced by:  simpl2l  992  simpr2l  998  simp12l  1052  simp22l  1058  simp32l  1064  issod  4082  funprg  4980  fsnunf  5394  f1oiso2  5497  ecopovtrn  6269  ecopovtrng  6272  addassnqg  6634  ltsonq  6650  ltanqg  6652  ltmnqg  6653  addassnq0  6714  recexprlem1ssu  6886  mulasssrg  6997  distrsrg  6998  lttrsr  7001  ltsosr  7003  ltasrg  7009  mulextsr1lem  7018  mulextsr1  7019  axmulass  7101  axdistr  7102  dmdcanap  7877  ltdiv2  8032  lediv2  8036  ltdiv23  8037  lediv23  8038  expaddzaplem  9616  expaddzap  9617  expmulzap  9619  expdivap  9624  prmexpb  10674