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  4354  funprg  5308  fsnunf  5762  f1oiso2  5874  ecopovtrn  6691  ecopovtrng  6694  dftap2  7318  addassnqg  7449  ltsonq  7465  ltanqg  7467  ltmnqg  7468  addassnq0  7529  recexprlem1ssu  7701  mulasssrg  7825  distrsrg  7826  lttrsr  7829  ltsosr  7831  ltasrg  7837  mulextsr1lem  7847  mulextsr1  7848  axmulass  7940  axdistr  7941  dmdcanap  8749  ltdiv2  8914  lediv2  8918  ltdiv23  8919  lediv23  8920  xaddass  9944  xaddass2  9945  xlt2add  9955  expaddzaplem  10674  expaddzap  10675  expmulzap  10677  expdivap  10682  leisorel  10929  bdtrilem  11404  bdtri  11405  xrbdtri  11441  fsumsplitsnun  11584  prmexpb  12319  pcpremul  12462  pcdiv  12471  pcqmul  12472  pcqdiv  12476  4sqlem12  12571  f1ocpbllem  12953  ercpbl  12974  erlecpbl  12975  cmn4  13435  ablsub4  13443  abladdsub4  13444  cnptoprest  14475  ssblps  14661  ssbl  14662  tgqioo  14791  plyadd  14987  plymul  14988  rplogbchbase  15186