Theorem simp2l 1047

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

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

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 1004

This theorem is referenced by:  simpl2l  1074  simpr2l  1080  simp12l  1134  simp22l  1140  simp32l  1146  issod  4411  funprg  5374  fsnunf  5846  f1oiso2  5960  ecopovtrn  6792  ecopovtrng  6795  dftap2  7453  addassnqg  7585  ltsonq  7601  ltanqg  7603  ltmnqg  7604  addassnq0  7665  recexprlem1ssu  7837  mulasssrg  7961  distrsrg  7962  lttrsr  7965  ltsosr  7967  ltasrg  7973  mulextsr1lem  7983  mulextsr1  7984  axmulass  8076  axdistr  8077  dmdcanap  8885  ltdiv2  9050  lediv2  9054  ltdiv23  9055  lediv23  9056  xaddass  10082  xaddass2  10083  xlt2add  10093  expaddzaplem  10821  expaddzap  10822  expmulzap  10824  expdivap  10829  leisorel  11077  swrdspsleq  11220  pfxeq  11249  ccatopth2  11270  bdtrilem  11771  bdtri  11772  xrbdtri  11808  fsumsplitsnun  11951  prmexpb  12694  pcpremul  12837  pcdiv  12846  pcqmul  12847  pcqdiv  12851  4sqlem12  12946  f1ocpbllem  13364  ercpbl  13385  erlecpbl  13386  cmn4  13863  ablsub4  13871  abladdsub4  13872  cnptoprest  14934  ssblps  15120  ssbl  15121  tgqioo  15250  plyadd  15446  plymul  15447  rplogbchbase  15645