Theorem simp3lr 1264

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

Assertion

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

Proof of Theorem simp3lr

Step	Hyp	Ref	Expression
1		simplr 781	. 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  7361  omeu  8579  ntrivcvgmul  15982  tsmsxp  24349  tgqioo  24994  ovolunlem2  25694  plyadd  26411  plymul  26412  coeeu  26419  nosupbnd1lem2  27910  noinfbnd1lem2  27925  tghilberti2  28948  btwnconn1lem2  36601  btwnconn1lem3  36602  btwnconn1lem4  36603  athgt  40271  2llnjN  40382  4atlem12b  40426  lncmp  40598  cdlema2N  40607  cdleme21ct  41144  cdleme24  41167  cdleme27a  41182  cdleme28  41188  cdleme42b  41293  cdlemf  41378  dihlsscpre  42049  dihord4  42073  dihord5apre  42077  pellex  43603  jm2.27  43776