Theorem simp2l 1050

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

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

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 1007

This theorem is referenced by:  simpl2l  1077  simpr2l  1083  simp12l  1137  simp22l  1143  simp32l  1149  issod  4442  funprg  5408  fsnunf  5886  f1oiso2  6002  ecopovtrn  6868  ecopovtrng  6871  dftap2  7570  addassnqg  7702  ltsonq  7718  ltanqg  7720  ltmnqg  7721  addassnq0  7782  recexprlem1ssu  7954  mulasssrg  8078  distrsrg  8079  lttrsr  8082  ltsosr  8084  ltasrg  8090  mulextsr1lem  8100  mulextsr1  8101  axmulass  8193  axdistr  8194  dmdcanap  9001  ltdiv2  9166  lediv2  9170  ltdiv23  9171  lediv23  9172  xaddass  10208  xaddass2  10209  xlt2add  10219  expaddzaplem  10951  expaddzap  10952  expmulzap  10954  expdivap  10959  leisorel  11217  swrdspsleq  11367  pfxeq  11396  ccatopth2  11417  bdtrilem  11932  bdtri  11933  xrbdtri  11969  fsumsplitsnun  12113  prmexpb  12856  pcpremul  12999  pcdiv  13008  pcqmul  13009  pcqdiv  13013  4sqlem12  13108  f1ocpbllem  13544  ercpbl  13565  erlecpbl  13566  cmn4  14043  ablsub4  14051  abladdsub4  14052  cnptoprest  15153  ssblps  15339  ssbl  15340  tgqioo  15469  plyadd  15665  plymul  15666  rplogbchbase  15864