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  4445  funprg  5411  fsnunf  5889  f1oiso2  6006  ecopovtrn  6879  ecopovtrng  6882  dftap2  7581  addassnqg  7713  ltsonq  7729  ltanqg  7731  ltmnqg  7732  addassnq0  7793  recexprlem1ssu  7965  mulasssrg  8089  distrsrg  8090  lttrsr  8093  ltsosr  8095  ltasrg  8101  mulextsr1lem  8111  mulextsr1  8112  axmulass  8204  axdistr  8205  dmdcanap  9016  ltdiv2  9181  lediv2  9185  ltdiv23  9186  lediv23  9187  xaddass  10224  xaddass2  10225  xlt2add  10235  expaddzaplem  10971  expaddzap  10972  expmulzap  10974  expdivap  10979  leisorel  11237  swrdspsleq  11387  pfxeq  11416  ccatopth2  11437  bdtrilem  11952  bdtri  11953  xrbdtri  11989  fsumsplitsnun  12133  prmexpb  12876  pcpremul  13019  pcdiv  13028  pcqmul  13029  pcqdiv  13033  4sqlem12  13128  f1ocpbllem  13577  ercpbl  13598  erlecpbl  13599  cmn4  14061  ablsub4  14069  abladdsub4  14070  rng1zrlem  14201  cnptoprest  15233  ssblps  15419  ssbl  15420  tgqioo  15549  plyadd  15745  plymul  15746  rplogbchbase  15944  dichmul0or  16643