Theorem simp3lr 1246

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

Assertion

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

Proof of Theorem simp3lr

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

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

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 1088

This theorem is referenced by:  f1oiso2  7298  omeu  8512  ntrivcvgmul  15825  tsmsxp  24099  tgqioo  24744  ovolunlem2  25455  plyadd  26178  plymul  26179  coeeu  26186  nosupbnd1lem2  27677  noinfbnd1lem2  27692  tghilberti2  28710  btwnconn1lem2  36282  btwnconn1lem3  36283  btwnconn1lem4  36284  athgt  39712  2llnjN  39823  4atlem12b  39867  lncmp  40039  cdlema2N  40048  cdleme21ct  40585  cdleme24  40608  cdleme27a  40623  cdleme28  40629  cdleme42b  40734  cdlemf  40819  dihlsscpre  41490  dihord4  41514  dihord5apre  41518  pellex  43073  jm2.27  43246