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  7361  omeu  8579  ntrivcvgmul  15982  tsmsxp  24349  tgqioo  24994  ovolunlem2  25694  plyadd  26411  plymul  26412  coeeu  26419  nosupbnd1lem2  27910  noinfbnd1lem2  27925  tghilberti2  28948  btwnconn1lem2  36601  btwnconn1lem3  36602  btwnconn1lem12  36611  athgt  40271  2llnjN  40382  4atlem12b  40426  lncmp  40598  cdlema2N  40607  cdlemc2  41007  cdleme5  41055  cdleme11a  41075  cdleme21ct  41144  cdleme21  41152  cdleme22eALTN  41160  cdleme24  41167  cdleme27cl  41181  cdleme27a  41182  cdleme28  41188  cdleme36a  41275  cdleme42b  41293  cdleme48fvg  41315  cdlemf  41378  cdlemk39  41731  cdlemkid1  41737  dihlsscpre  42049  dihord4  42073  dihord5apre  42077  dihmeetlem20N  42141  mapdh9a  42604  pellex  43603  jm2.27  43776