Theorem simp2l 1047

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

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

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 1004

This theorem is referenced by:  simpl2l  1074  simpr2l  1080  simp12l  1134  simp22l  1140  simp32l  1146  issod  4410  funprg  5371  fsnunf  5843  f1oiso2  5957  ecopovtrn  6787  ecopovtrng  6790  dftap2  7445  addassnqg  7577  ltsonq  7593  ltanqg  7595  ltmnqg  7596  addassnq0  7657  recexprlem1ssu  7829  mulasssrg  7953  distrsrg  7954  lttrsr  7957  ltsosr  7959  ltasrg  7965  mulextsr1lem  7975  mulextsr1  7976  axmulass  8068  axdistr  8069  dmdcanap  8877  ltdiv2  9042  lediv2  9046  ltdiv23  9047  lediv23  9048  xaddass  10073  xaddass2  10074  xlt2add  10084  expaddzaplem  10812  expaddzap  10813  expmulzap  10815  expdivap  10820  leisorel  11067  swrdspsleq  11207  pfxeq  11236  ccatopth2  11257  bdtrilem  11758  bdtri  11759  xrbdtri  11795  fsumsplitsnun  11938  prmexpb  12681  pcpremul  12824  pcdiv  12833  pcqmul  12834  pcqdiv  12838  4sqlem12  12933  f1ocpbllem  13351  ercpbl  13372  erlecpbl  13373  cmn4  13850  ablsub4  13858  abladdsub4  13859  cnptoprest  14921  ssblps  15107  ssbl  15108  tgqioo  15237  plyadd  15433  plymul  15434  rplogbchbase  15632