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

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

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 1011

This theorem is referenced by:  simpl2l  1081  simpr2l  1087  simp12l  1141  simp22l  1147  simp32l  1153  issod  4462  funprg  5429  fsnunf  5909  f1oiso2  6027  ecopovtrn  6900  ecopovtrng  6903  dftap2  7611  addassnqg  7743  ltsonq  7759  ltanqg  7761  ltmnqg  7762  addassnq0  7823  recexprlem1ssu  7995  mulasssrg  8119  distrsrg  8120  lttrsr  8123  ltsosr  8125  ltasrg  8131  mulextsr1lem  8141  mulextsr1  8142  axmulass  8234  axdistr  8235  dmdcanap  9046  ltdiv2  9211  lediv2  9215  ltdiv23  9216  lediv23  9217  xaddass  10254  xaddass2  10255  xlt2add  10265  expaddzaplem  11002  expaddzap  11003  expmulzap  11005  expdivap  11010  leisorel  11272  swrdspsleq  11422  pfxeq  11451  ccatopth2  11472  bdtrilem  11988  bdtri  11989  xrbdtri  12025  fsumsplitsnun  12169  prmexpb  12912  pcpremul  13055  pcdiv  13064  pcqmul  13065  pcqdiv  13069  4sqlem12  13164  f1ocpbllem  13614  ercpbl  13635  erlecpbl  13636  cmn4  14091  ablsub4  14100  abladdsub4  14101  rng1zrlem  14241  cnptoprest  15323  ssblps  15509  ssbl  15510  tgqioo  15639  plyadd  15835  plymul  15836  rplogbchbase  16035  dichmul0or  16743