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 767	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑)
2	1	3ad2ant3 1134	1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  f1oiso2  7372  omeu  8622  ntrivcvgmul  15935  tsmsxp  24179  tgqioo  24836  ovolunlem2  25547  plyadd  26271  plymul  26272  coeeu  26279  nosupbnd1lem2  27769  noinfbnd1lem2  27784  tghilberti2  28661  btwnconn1lem2  36070  btwnconn1lem3  36071  btwnconn1lem12  36080  athgt  39439  2llnjN  39550  4atlem12b  39594  lncmp  39766  cdlema2N  39775  cdlemc2  40175  cdleme5  40223  cdleme11a  40243  cdleme21ct  40312  cdleme21  40320  cdleme22eALTN  40328  cdleme24  40335  cdleme27cl  40349  cdleme27a  40350  cdleme28  40356  cdleme36a  40443  cdleme42b  40461  cdleme48fvg  40483  cdlemf  40546  cdlemk39  40899  cdlemkid1  40905  dihlsscpre  41217  dihord4  41241  dihord5apre  41245  dihmeetlem20N  41309  mapdh9a  41772  pellex  42823  jm2.27  42997