Theorem simp3ll 1244

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

Assertion

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

Proof of Theorem simp3ll

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  f1oiso2  7388  omeu  8641  ntrivcvgmul  15950  tsmsxp  24184  tgqioo  24841  ovolunlem2  25552  plyadd  26276  plymul  26277  coeeu  26284  nosupbnd1lem2  27772  noinfbnd1lem2  27787  tghilberti2  28664  btwnconn1lem2  36052  btwnconn1lem3  36053  btwnconn1lem12  36062  athgt  39413  2llnjN  39524  4atlem12b  39568  lncmp  39740  cdlema2N  39749  cdlemc2  40149  cdleme5  40197  cdleme11a  40217  cdleme21ct  40286  cdleme21  40294  cdleme22eALTN  40302  cdleme24  40309  cdleme27cl  40323  cdleme27a  40324  cdleme28  40330  cdleme36a  40417  cdleme42b  40435  cdleme48fvg  40457  cdlemf  40520  cdlemk39  40873  cdlemkid1  40879  dihlsscpre  41191  dihord4  41215  dihord5apre  41219  dihmeetlem20N  41283  mapdh9a  41746  pellex  42791  jm2.27  42965