Theorem simp2l 1049

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

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

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 1006

This theorem is referenced by:  simpl2l  1076  simpr2l  1082  simp12l  1136  simp22l  1142  simp32l  1148  issod  4418  funprg  5382  fsnunf  5857  f1oiso2  5973  ecopovtrn  6806  ecopovtrng  6809  dftap2  7475  addassnqg  7607  ltsonq  7623  ltanqg  7625  ltmnqg  7626  addassnq0  7687  recexprlem1ssu  7859  mulasssrg  7983  distrsrg  7984  lttrsr  7987  ltsosr  7989  ltasrg  7995  mulextsr1lem  8005  mulextsr1  8006  axmulass  8098  axdistr  8099  dmdcanap  8907  ltdiv2  9072  lediv2  9076  ltdiv23  9077  lediv23  9078  xaddass  10109  xaddass2  10110  xlt2add  10120  expaddzaplem  10850  expaddzap  10851  expmulzap  10853  expdivap  10858  leisorel  11107  swrdspsleq  11257  pfxeq  11286  ccatopth2  11307  bdtrilem  11822  bdtri  11823  xrbdtri  11859  fsumsplitsnun  12003  prmexpb  12746  pcpremul  12889  pcdiv  12898  pcqmul  12899  pcqdiv  12903  4sqlem12  12998  f1ocpbllem  13416  ercpbl  13437  erlecpbl  13438  cmn4  13915  ablsub4  13923  abladdsub4  13924  cnptoprest  14992  ssblps  15178  ssbl  15179  tgqioo  15308  plyadd  15504  plymul  15505  rplogbchbase  15703