Theorem simp2l 1054

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl2l  1081  simpr2l  1087  simp12l  1141  simp22l  1147  simp32l  1153  issod  4466  funprg  5434  fsnunf  5918  f1oiso2  6036  ecopovtrn  6910  ecopovtrng  6913  dftap2  7624  addassnqg  7756  ltsonq  7772  ltanqg  7774  ltmnqg  7775  addassnq0  7836  recexprlem1ssu  8008  mulasssrg  8132  distrsrg  8133  lttrsr  8136  ltsosr  8138  ltasrg  8144  mulextsr1lem  8154  mulextsr1  8155  axmulass  8247  axdistr  8248  dmdcanap  9061  ltdiv2  9226  lediv2  9230  ltdiv23  9231  lediv23  9232  xaddass  10289  xaddass2  10290  xlt2add  10300  expaddzaplem  11041  expaddzap  11042  expmulzap  11044  expdivap  11049  leisorel  11312  swrdspsleq  11462  pfxeq  11491  ccatopth2  11512  bdtrilem  12031  bdtri  12032  xrbdtri  12068  fsumsplitsnun  12212  prmexpb  12956  pcpremul  13102  pcdiv  13111  pcqmul  13112  pcqdiv  13116  4sqlem12  13211  f1ocpbllem  13691  ercpbl  13712  erlecpbl  13713  cmn4  14199  ablsub4  14208  abladdsub4  14209  rng1zrlem  14366  cnptoprest  15477  ssblps  15663  ssbl  15664  tgqioo  15793  plyadd  15989  plymul  15990  rplogbchbase  16198  dichmul0or  16977