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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  f1oiso2  7352  omeu  8571  ntrivcvgmul  15958  tsmsxp  24293  tgqioo  24938  ovolunlem2  25638  plyadd  26355  plymul  26356  coeeu  26363  nosupbnd1lem2  27851  noinfbnd1lem2  27866  tghilberti2  28889  btwnconn1lem2  36558  btwnconn1lem3  36559  btwnconn1lem12  36568  athgt  40208  2llnjN  40319  4atlem12b  40363  lncmp  40535  cdlema2N  40544  cdlemc2  40944  cdleme5  40992  cdleme11a  41012  cdleme21ct  41081  cdleme21  41089  cdleme22eALTN  41097  cdleme24  41104  cdleme27cl  41118  cdleme27a  41119  cdleme28  41125  cdleme36a  41212  cdleme42b  41230  cdleme48fvg  41252  cdlemf  41315  cdlemk39  41668  cdlemkid1  41674  dihlsscpre  41986  dihord4  42010  dihord5apre  42014  dihmeetlem20N  42078  mapdh9a  42541  pellex  43542  jm2.27  43715