Theorem simp3lr 1258

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

Assertion

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

Proof of Theorem simp3lr

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  f1oiso2  7332  omeu  8549  ntrivcvgmul  15915  tsmsxp  24195  tgqioo  24840  ovolunlem2  25540  plyadd  26257  plymul  26258  coeeu  26265  nosupbnd1lem2  27750  noinfbnd1lem2  27765  tghilberti2  28784  btwnconn1lem2  36402  btwnconn1lem3  36403  btwnconn1lem4  36404  athgt  40044  2llnjN  40155  4atlem12b  40199  lncmp  40371  cdlema2N  40380  cdleme21ct  40917  cdleme24  40940  cdleme27a  40955  cdleme28  40961  cdleme42b  41066  cdlemf  41151  dihlsscpre  41822  dihord4  41846  dihord5apre  41850  pellex  43376  jm2.27  43549