Theorem simp2l 1018

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 108	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	3ad2ant2 1014	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  simpl2l  1045  simpr2l  1051  simp12l  1105  simp22l  1111  simp32l  1117  issod  4302  funprg  5246  fsnunf  5694  f1oiso2  5804  ecopovtrn  6607  ecopovtrng  6610  addassnqg  7333  ltsonq  7349  ltanqg  7351  ltmnqg  7352  addassnq0  7413  recexprlem1ssu  7585  mulasssrg  7709  distrsrg  7710  lttrsr  7713  ltsosr  7715  ltasrg  7721  mulextsr1lem  7731  mulextsr1  7732  axmulass  7824  axdistr  7825  dmdcanap  8628  ltdiv2  8792  lediv2  8796  ltdiv23  8797  lediv23  8798  xaddass  9815  xaddass2  9816  xlt2add  9826  expaddzaplem  10508  expaddzap  10509  expmulzap  10511  expdivap  10516  leisorel  10761  bdtrilem  11191  bdtri  11192  xrbdtri  11228  fsumsplitsnun  11371  prmexpb  12094  pcpremul  12236  pcdiv  12245  pcqmul  12246  pcqdiv  12250  cnptoprest  12994  ssblps  13180  ssbl  13181  tgqioo  13302  rplogbchbase  13623