Theorem simp2l 1026

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

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

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 983

This theorem is referenced by:  simpl2l  1053  simpr2l  1059  simp12l  1113  simp22l  1119  simp32l  1125  issod  4370  funprg  5329  fsnunf  5791  f1oiso2  5903  ecopovtrn  6726  ecopovtrng  6729  dftap2  7370  addassnqg  7502  ltsonq  7518  ltanqg  7520  ltmnqg  7521  addassnq0  7582  recexprlem1ssu  7754  mulasssrg  7878  distrsrg  7879  lttrsr  7882  ltsosr  7884  ltasrg  7890  mulextsr1lem  7900  mulextsr1  7901  axmulass  7993  axdistr  7994  dmdcanap  8802  ltdiv2  8967  lediv2  8971  ltdiv23  8972  lediv23  8973  xaddass  9998  xaddass2  9999  xlt2add  10009  expaddzaplem  10734  expaddzap  10735  expmulzap  10737  expdivap  10742  leisorel  10989  swrdspsleq  11128  pfxeq  11155  bdtrilem  11594  bdtri  11595  xrbdtri  11631  fsumsplitsnun  11774  prmexpb  12517  pcpremul  12660  pcdiv  12669  pcqmul  12670  pcqdiv  12674  4sqlem12  12769  f1ocpbllem  13186  ercpbl  13207  erlecpbl  13208  cmn4  13685  ablsub4  13693  abladdsub4  13694  cnptoprest  14755  ssblps  14941  ssbl  14942  tgqioo  15071  plyadd  15267  plymul  15268  rplogbchbase  15466