Theorem simp3ll 1251

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

Assertion

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

Proof of Theorem simp3ll

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

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

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  f1oiso2  7303  omeu  8517  ntrivcvgmul  15865  tsmsxp  24145  tgqioo  24790  ovolunlem2  25490  plyadd  26207  plymul  26208  coeeu  26215  nosupbnd1lem2  27698  noinfbnd1lem2  27713  tghilberti2  28731  btwnconn1lem2  36323  btwnconn1lem3  36324  btwnconn1lem12  36333  athgt  39955  2llnjN  40066  4atlem12b  40110  lncmp  40282  cdlema2N  40291  cdlemc2  40691  cdleme5  40739  cdleme11a  40759  cdleme21ct  40828  cdleme21  40836  cdleme22eALTN  40844  cdleme24  40851  cdleme27cl  40865  cdleme27a  40866  cdleme28  40872  cdleme36a  40959  cdleme42b  40977  cdleme48fvg  40999  cdlemf  41062  cdlemk39  41415  cdlemkid1  41421  dihlsscpre  41733  dihord4  41757  dihord5apre  41761  dihmeetlem20N  41825  mapdh9a  42288  pellex  43287  jm2.27  43460