Theorem simp3ll 1243

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp3ll	⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑)

Proof of Theorem simp3ll

Step	Hyp	Ref	Expression
1		simpll 764	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant3 1134	1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088

This theorem is referenced by:  f1oiso2  7223  omeu  8416  ntrivcvgmul  15614  tsmsxp  23306  tgqioo  23963  ovolunlem2  24662  plyadd  25378  plymul  25379  coeeu  25386  tghilberti2  26999  nosupbnd1lem2  33912  noinfbnd1lem2  33927  btwnconn1lem2  34390  btwnconn1lem3  34391  btwnconn1lem12  34400  athgt  37470  2llnjN  37581  4atlem12b  37625  lncmp  37797  cdlema2N  37806  cdlemc2  38206  cdleme5  38254  cdleme11a  38274  cdleme21ct  38343  cdleme21  38351  cdleme22eALTN  38359  cdleme24  38366  cdleme27cl  38380  cdleme27a  38381  cdleme28  38387  cdleme36a  38474  cdleme42b  38492  cdleme48fvg  38514  cdlemf  38577  cdlemk39  38930  cdlemkid1  38936  dihlsscpre  39248  dihord4  39272  dihord5apre  39276  dihmeetlem20N  39340  mapdh9a  39803  pellex  40657  jm2.27  40830