Theorem simp2l 1025

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

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

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 982

This theorem is referenced by:  simpl2l  1052  simpr2l  1058  simp12l  1112  simp22l  1118  simp32l  1124  issod  4337  funprg  5285  fsnunf  5736  f1oiso2  5848  ecopovtrn  6657  ecopovtrng  6660  dftap2  7279  addassnqg  7410  ltsonq  7426  ltanqg  7428  ltmnqg  7429  addassnq0  7490  recexprlem1ssu  7662  mulasssrg  7786  distrsrg  7787  lttrsr  7790  ltsosr  7792  ltasrg  7798  mulextsr1lem  7808  mulextsr1  7809  axmulass  7901  axdistr  7902  dmdcanap  8708  ltdiv2  8873  lediv2  8877  ltdiv23  8878  lediv23  8879  xaddass  9898  xaddass2  9899  xlt2add  9909  expaddzaplem  10593  expaddzap  10594  expmulzap  10596  expdivap  10601  leisorel  10848  bdtrilem  11278  bdtri  11279  xrbdtri  11315  fsumsplitsnun  11458  prmexpb  12182  pcpremul  12324  pcdiv  12333  pcqmul  12334  pcqdiv  12338  4sqlem12  12433  f1ocpbllem  12784  ercpbl  12804  erlecpbl  12805  cmn4  13241  ablsub4  13249  abladdsub4  13250  cnptoprest  14191  ssblps  14377  ssbl  14378  tgqioo  14499  rplogbchbase  14820