Theorem simp2l 975

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

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

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

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

This theorem is referenced by:  simpl2l  1002  simpr2l  1008  simp12l  1062  simp22l  1068  simp32l  1074  issod  4179  funprg  5109  fsnunf  5552  f1oiso2  5660  ecopovtrn  6456  ecopovtrng  6459  addassnqg  7091  ltsonq  7107  ltanqg  7109  ltmnqg  7110  addassnq0  7171  recexprlem1ssu  7343  mulasssrg  7454  distrsrg  7455  lttrsr  7458  ltsosr  7460  ltasrg  7466  mulextsr1lem  7475  mulextsr1  7476  axmulass  7558  axdistr  7559  dmdcanap  8343  ltdiv2  8503  lediv2  8507  ltdiv23  8508  lediv23  8509  xaddass  9493  xaddass2  9494  xlt2add  9504  expaddzaplem  10177  expaddzap  10178  expmulzap  10180  expdivap  10185  leisorel  10421  bdtrilem  10849  bdtri  10850  xrbdtri  10884  fsumsplitsnun  11027  prmexpb  11622  cnptoprest  12189  ssblps  12353  ssbl  12354  tgqioo  12466