Theorem simp2l 1007

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simpl2l  1034  simpr2l  1040  simp12l  1094  simp22l  1100  simp32l  1106  issod  4236  funprg  5168  fsnunf  5613  f1oiso2  5721  ecopovtrn  6519  ecopovtrng  6522  addassnqg  7183  ltsonq  7199  ltanqg  7201  ltmnqg  7202  addassnq0  7263  recexprlem1ssu  7435  mulasssrg  7559  distrsrg  7560  lttrsr  7563  ltsosr  7565  ltasrg  7571  mulextsr1lem  7581  mulextsr1  7582  axmulass  7674  axdistr  7675  dmdcanap  8475  ltdiv2  8638  lediv2  8642  ltdiv23  8643  lediv23  8644  xaddass  9645  xaddass2  9646  xlt2add  9656  expaddzaplem  10329  expaddzap  10330  expmulzap  10332  expdivap  10337  leisorel  10573  bdtrilem  11003  bdtri  11004  xrbdtri  11038  fsumsplitsnun  11181  prmexpb  11818  cnptoprest  12397  ssblps  12583  ssbl  12584  tgqioo  12705