Theorem simp2l 1050

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

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

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 1007

This theorem is referenced by:  simpl2l  1077  simpr2l  1083  simp12l  1137  simp22l  1143  simp32l  1149  issod  4442  funprg  5408  fsnunf  5886  f1oiso2  6002  ecopovtrn  6868  ecopovtrng  6871  dftap2  7567  addassnqg  7699  ltsonq  7715  ltanqg  7717  ltmnqg  7718  addassnq0  7779  recexprlem1ssu  7951  mulasssrg  8075  distrsrg  8076  lttrsr  8079  ltsosr  8081  ltasrg  8087  mulextsr1lem  8097  mulextsr1  8098  axmulass  8190  axdistr  8191  dmdcanap  8998  ltdiv2  9163  lediv2  9167  ltdiv23  9168  lediv23  9169  xaddass  10205  xaddass2  10206  xlt2add  10216  expaddzaplem  10948  expaddzap  10949  expmulzap  10951  expdivap  10956  leisorel  11213  swrdspsleq  11363  pfxeq  11392  ccatopth2  11413  bdtrilem  11928  bdtri  11929  xrbdtri  11965  fsumsplitsnun  12109  prmexpb  12852  pcpremul  12995  pcdiv  13004  pcqmul  13005  pcqdiv  13009  4sqlem12  13104  f1ocpbllem  13540  ercpbl  13561  erlecpbl  13562  cmn4  14039  ablsub4  14047  abladdsub4  14048  cnptoprest  15121  ssblps  15307  ssbl  15308  tgqioo  15437  plyadd  15633  plymul  15634  rplogbchbase  15832