Theorem simp2l 1025

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

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

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 982

This theorem is referenced by:  simpl2l  1052  simpr2l  1058  simp12l  1112  simp22l  1118  simp32l  1124  issod  4355  funprg  5309  fsnunf  5765  f1oiso2  5877  ecopovtrn  6700  ecopovtrng  6703  dftap2  7334  addassnqg  7466  ltsonq  7482  ltanqg  7484  ltmnqg  7485  addassnq0  7546  recexprlem1ssu  7718  mulasssrg  7842  distrsrg  7843  lttrsr  7846  ltsosr  7848  ltasrg  7854  mulextsr1lem  7864  mulextsr1  7865  axmulass  7957  axdistr  7958  dmdcanap  8766  ltdiv2  8931  lediv2  8935  ltdiv23  8936  lediv23  8937  xaddass  9961  xaddass2  9962  xlt2add  9972  expaddzaplem  10691  expaddzap  10692  expmulzap  10694  expdivap  10699  leisorel  10946  bdtrilem  11421  bdtri  11422  xrbdtri  11458  fsumsplitsnun  11601  prmexpb  12344  pcpremul  12487  pcdiv  12496  pcqmul  12497  pcqdiv  12501  4sqlem12  12596  f1ocpbllem  13012  ercpbl  13033  erlecpbl  13034  cmn4  13511  ablsub4  13519  abladdsub4  13520  cnptoprest  14559  ssblps  14745  ssbl  14746  tgqioo  14875  plyadd  15071  plymul  15072  rplogbchbase  15270