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  4439  funprg  5405  fsnunf  5883  f1oiso2  5999  ecopovtrn  6865  ecopovtrng  6868  dftap2  7561  addassnqg  7693  ltsonq  7709  ltanqg  7711  ltmnqg  7712  addassnq0  7773  recexprlem1ssu  7945  mulasssrg  8069  distrsrg  8070  lttrsr  8073  ltsosr  8075  ltasrg  8081  mulextsr1lem  8091  mulextsr1  8092  axmulass  8184  axdistr  8185  dmdcanap  8992  ltdiv2  9157  lediv2  9161  ltdiv23  9162  lediv23  9163  xaddass  10198  xaddass2  10199  xlt2add  10209  expaddzaplem  10940  expaddzap  10941  expmulzap  10943  expdivap  10948  leisorel  11202  swrdspsleq  11352  pfxeq  11381  ccatopth2  11402  bdtrilem  11917  bdtri  11918  xrbdtri  11954  fsumsplitsnun  12098  prmexpb  12841  pcpremul  12984  pcdiv  12993  pcqmul  12994  pcqdiv  12998  4sqlem12  13093  f1ocpbllem  13512  ercpbl  13533  erlecpbl  13534  cmn4  14011  ablsub4  14019  abladdsub4  14020  cnptoprest  15091  ssblps  15277  ssbl  15278  tgqioo  15407  plyadd  15603  plymul  15604  rplogbchbase  15802