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  7360  omeu  8596  ntrivcvgmul  16076  tsmsxp  24479  tgqioo  25124  ovolunlem2  25824  plyadd  26541  plymul  26542  coeeu  26549  nosupbnd1lem2  28071  noinfbnd1lem2  28086  tghilberti2  29111  btwnconn1lem2  36945  btwnconn1lem3  36946  btwnconn1lem12  36955  athgt  40606  2llnjN  40717  4atlem12b  40761  lncmp  40933  cdlema2N  40942  cdlemc2  41342  cdleme5  41390  cdleme11a  41410  cdleme21ct  41479  cdleme21  41487  cdleme22eALTN  41495  cdleme24  41502  cdleme27cl  41516  cdleme27a  41517  cdleme28  41523  cdleme36a  41610  cdleme42b  41628  cdleme48fvg  41650  cdlemf  41713  cdlemk39  42066  cdlemkid1  42072  dihlsscpre  42384  dihord4  42408  dihord5apre  42412  dihmeetlem20N  42476  mapdh9a  42939  pellex  43935  jm2.27  44108