Theorem simp3lr 1262

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

Assertion

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

Proof of Theorem simp3lr

Step	Hyp	Ref	Expression
1		simplr 780	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
2	1	3ad2ant3 1151	1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜓)

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

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 1103

This theorem is referenced by:  f1oiso2  7340  omeu  8558  ntrivcvgmul  15946  tsmsxp  24273  tgqioo  24918  ovolunlem2  25618  plyadd  26335  plymul  26336  coeeu  26343  nosupbnd1lem2  27831  noinfbnd1lem2  27846  tghilberti2  28865  btwnconn1lem2  36451  btwnconn1lem3  36452  btwnconn1lem4  36453  athgt  40092  2llnjN  40203  4atlem12b  40247  lncmp  40419  cdlema2N  40428  cdleme21ct  40965  cdleme24  40988  cdleme27a  41003  cdleme28  41009  cdleme42b  41114  cdlemf  41199  dihlsscpre  41870  dihord4  41894  dihord5apre  41898  pellex  43424  jm2.27  43597