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  4414  funprg  5377  fsnunf  5849  f1oiso2  5963  ecopovtrn  6796  ecopovtrng  6799  dftap2  7463  addassnqg  7595  ltsonq  7611  ltanqg  7613  ltmnqg  7614  addassnq0  7675  recexprlem1ssu  7847  mulasssrg  7971  distrsrg  7972  lttrsr  7975  ltsosr  7977  ltasrg  7983  mulextsr1lem  7993  mulextsr1  7994  axmulass  8086  axdistr  8087  dmdcanap  8895  ltdiv2  9060  lediv2  9064  ltdiv23  9065  lediv23  9066  xaddass  10097  xaddass2  10098  xlt2add  10108  expaddzaplem  10837  expaddzap  10838  expmulzap  10840  expdivap  10845  leisorel  11094  swrdspsleq  11241  pfxeq  11270  ccatopth2  11291  bdtrilem  11793  bdtri  11794  xrbdtri  11830  fsumsplitsnun  11973  prmexpb  12716  pcpremul  12859  pcdiv  12868  pcqmul  12869  pcqdiv  12873  4sqlem12  12968  f1ocpbllem  13386  ercpbl  13407  erlecpbl  13408  cmn4  13885  ablsub4  13893  abladdsub4  13894  cnptoprest  14956  ssblps  15142  ssbl  15143  tgqioo  15272  plyadd  15468  plymul  15469  rplogbchbase  15667