Theorem simp2l 1023

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

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

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 980

This theorem is referenced by:  simpl2l  1050  simpr2l  1056  simp12l  1110  simp22l  1116  simp32l  1122  issod  4320  funprg  5267  fsnunf  5717  f1oiso2  5828  ecopovtrn  6632  ecopovtrng  6635  dftap2  7250  addassnqg  7381  ltsonq  7397  ltanqg  7399  ltmnqg  7400  addassnq0  7461  recexprlem1ssu  7633  mulasssrg  7757  distrsrg  7758  lttrsr  7761  ltsosr  7763  ltasrg  7769  mulextsr1lem  7779  mulextsr1  7780  axmulass  7872  axdistr  7873  dmdcanap  8679  ltdiv2  8844  lediv2  8848  ltdiv23  8849  lediv23  8850  xaddass  9869  xaddass2  9870  xlt2add  9880  expaddzaplem  10563  expaddzap  10564  expmulzap  10566  expdivap  10571  leisorel  10817  bdtrilem  11247  bdtri  11248  xrbdtri  11284  fsumsplitsnun  11427  prmexpb  12151  pcpremul  12293  pcdiv  12302  pcqmul  12303  pcqdiv  12307  f1ocpbllem  12731  ercpbl  12750  erlecpbl  12751  cmn4  13108  ablsub4  13116  abladdsub4  13117  cnptoprest  13742  ssblps  13928  ssbl  13929  tgqioo  14050  rplogbchbase  14371