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  7336  addassnqg  7468  ltsonq  7484  ltanqg  7486  ltmnqg  7487  addassnq0  7548  recexprlem1ssu  7720  mulasssrg  7844  distrsrg  7845  lttrsr  7848  ltsosr  7850  ltasrg  7856  mulextsr1lem  7866  mulextsr1  7867  axmulass  7959  axdistr  7960  dmdcanap  8768  ltdiv2  8933  lediv2  8937  ltdiv23  8938  lediv23  8939  xaddass  9963  xaddass2  9964  xlt2add  9974  expaddzaplem  10693  expaddzap  10694  expmulzap  10696  expdivap  10701  leisorel  10948  bdtrilem  11423  bdtri  11424  xrbdtri  11460  fsumsplitsnun  11603  prmexpb  12346  pcpremul  12489  pcdiv  12498  pcqmul  12499  pcqdiv  12503  4sqlem12  12598  f1ocpbllem  13014  ercpbl  13035  erlecpbl  13036  cmn4  13513  ablsub4  13521  abladdsub4  13522  cnptoprest  14583  ssblps  14769  ssbl  14770  tgqioo  14899  plyadd  15095  plymul  15096  rplogbchbase  15294