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  4319  funprg  5266  fsnunf  5716  f1oiso2  5827  ecopovtrn  6631  ecopovtrng  6634  dftap2  7249  addassnqg  7380  ltsonq  7396  ltanqg  7398  ltmnqg  7399  addassnq0  7460  recexprlem1ssu  7632  mulasssrg  7756  distrsrg  7757  lttrsr  7760  ltsosr  7762  ltasrg  7768  mulextsr1lem  7778  mulextsr1  7779  axmulass  7871  axdistr  7872  dmdcanap  8678  ltdiv2  8843  lediv2  8847  ltdiv23  8848  lediv23  8849  xaddass  9868  xaddass2  9869  xlt2add  9879  expaddzaplem  10562  expaddzap  10563  expmulzap  10565  expdivap  10570  leisorel  10816  bdtrilem  11246  bdtri  11247  xrbdtri  11283  fsumsplitsnun  11426  prmexpb  12150  pcpremul  12292  pcdiv  12301  pcqmul  12302  pcqdiv  12306  f1ocpbllem  12730  ercpbl  12749  erlecpbl  12750  cmn4  13106  ablsub4  13114  abladdsub4  13115  cnptoprest  13709  ssblps  13895  ssbl  13896  tgqioo  14017  rplogbchbase  14338