Theorem simp2l 1049

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1004

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

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  simpl2l  1076  simpr2l  1082  simp12l  1136  simp22l  1142  simp32l  1148  issod  4416  funprg  5380  fsnunf  5854  f1oiso2  5968  ecopovtrn  6801  ecopovtrng  6804  dftap2  7470  addassnqg  7602  ltsonq  7618  ltanqg  7620  ltmnqg  7621  addassnq0  7682  recexprlem1ssu  7854  mulasssrg  7978  distrsrg  7979  lttrsr  7982  ltsosr  7984  ltasrg  7990  mulextsr1lem  8000  mulextsr1  8001  axmulass  8093  axdistr  8094  dmdcanap  8902  ltdiv2  9067  lediv2  9071  ltdiv23  9072  lediv23  9073  xaddass  10104  xaddass2  10105  xlt2add  10115  expaddzaplem  10845  expaddzap  10846  expmulzap  10848  expdivap  10853  leisorel  11102  swrdspsleq  11249  pfxeq  11278  ccatopth2  11299  bdtrilem  11801  bdtri  11802  xrbdtri  11838  fsumsplitsnun  11982  prmexpb  12725  pcpremul  12868  pcdiv  12877  pcqmul  12878  pcqdiv  12882  4sqlem12  12977  f1ocpbllem  13395  ercpbl  13416  erlecpbl  13417  cmn4  13894  ablsub4  13902  abladdsub4  13903  cnptoprest  14966  ssblps  15152  ssbl  15153  tgqioo  15282  plyadd  15478  plymul  15479  rplogbchbase  15677