Theorem simp2l 1028

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

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

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 985

This theorem is referenced by:  simpl2l  1055  simpr2l  1061  simp12l  1115  simp22l  1121  simp32l  1127  issod  4387  funprg  5347  fsnunf  5812  f1oiso2  5924  ecopovtrn  6749  ecopovtrng  6752  dftap2  7405  addassnqg  7537  ltsonq  7553  ltanqg  7555  ltmnqg  7556  addassnq0  7617  recexprlem1ssu  7789  mulasssrg  7913  distrsrg  7914  lttrsr  7917  ltsosr  7919  ltasrg  7925  mulextsr1lem  7935  mulextsr1  7936  axmulass  8028  axdistr  8029  dmdcanap  8837  ltdiv2  9002  lediv2  9006  ltdiv23  9007  lediv23  9008  xaddass  10033  xaddass2  10034  xlt2add  10044  expaddzaplem  10771  expaddzap  10772  expmulzap  10774  expdivap  10779  leisorel  11026  swrdspsleq  11165  pfxeq  11194  ccatopth2  11215  bdtrilem  11716  bdtri  11717  xrbdtri  11753  fsumsplitsnun  11896  prmexpb  12639  pcpremul  12782  pcdiv  12791  pcqmul  12792  pcqdiv  12796  4sqlem12  12891  f1ocpbllem  13309  ercpbl  13330  erlecpbl  13331  cmn4  13808  ablsub4  13816  abladdsub4  13817  cnptoprest  14878  ssblps  15064  ssbl  15065  tgqioo  15194  plyadd  15390  plymul  15391  rplogbchbase  15589