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  4464  funprg  5431  fsnunf  5915  f1oiso2  6033  ecopovtrn  6906  ecopovtrng  6909  dftap2  7617  addassnqg  7749  ltsonq  7765  ltanqg  7767  ltmnqg  7768  addassnq0  7829  recexprlem1ssu  8001  mulasssrg  8125  distrsrg  8126  lttrsr  8129  ltsosr  8131  ltasrg  8137  mulextsr1lem  8147  mulextsr1  8148  axmulass  8240  axdistr  8241  dmdcanap  9053  ltdiv2  9218  lediv2  9222  ltdiv23  9223  lediv23  9224  xaddass  10273  xaddass2  10274  xlt2add  10284  expaddzaplem  11021  expaddzap  11022  expmulzap  11024  expdivap  11029  leisorel  11291  swrdspsleq  11441  pfxeq  11470  ccatopth2  11491  bdtrilem  12007  bdtri  12008  xrbdtri  12044  fsumsplitsnun  12188  prmexpb  12931  pcpremul  13074  pcdiv  13083  pcqmul  13084  pcqdiv  13088  4sqlem12  13183  f1ocpbllem  13633  ercpbl  13654  erlecpbl  13655  cmn4  14110  ablsub4  14119  abladdsub4  14120  rng1zrlem  14260  cnptoprest  15342  ssblps  15528  ssbl  15529  tgqioo  15658  plyadd  15854  plymul  15855  rplogbchbase  16058  dichmul0or  16772