Theorem simp3ll 1263

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

Assertion

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

Proof of Theorem simp3ll

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1oiso2  7383  omeu  8621  ntrivcvgmul  16100  tsmsxp  24504  tgqioo  25149  ovolunlem2  25849  plyadd  26566  plymul  26567  coeeu  26574  nosupbnd1lem2  28096  noinfbnd1lem2  28111  tghilberti2  29136  btwnconn1lem2  37031  btwnconn1lem3  37032  btwnconn1lem12  37041  athgt  40705  2llnjN  40816  4atlem12b  40860  lncmp  41032  cdlema2N  41041  cdlemc2  41441  cdleme5  41489  cdleme11a  41509  cdleme21ct  41578  cdleme21  41586  cdleme22eALTN  41594  cdleme24  41601  cdleme27cl  41615  cdleme27a  41616  cdleme28  41622  cdleme36a  41709  cdleme42b  41727  cdleme48fvg  41749  cdlemf  41812  cdlemk39  42165  cdlemkid1  42171  dihlsscpre  42483  dihord4  42507  dihord5apre  42511  dihmeetlem20N  42575  mapdh9a  43038  pellex  44035  jm2.27  44208