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  7383  omeu  8621  ntrivcvgmul  16100  tsmsxp  24504  tgqioo  25149  ovolunlem2  25849  plyadd  26566  plymul  26567  coeeu  26574  nosupbnd1lem2  28096  noinfbnd1lem2  28111  tghilberti2  29136  btwnconn1lem2  37031  btwnconn1lem3  37032  btwnconn1lem4  37033  athgt  40705  2llnjN  40816  4atlem12b  40860  lncmp  41032  cdlema2N  41041  cdleme21ct  41578  cdleme24  41601  cdleme27a  41616  cdleme28  41622  cdleme42b  41727  cdlemf  41812  dihlsscpre  42483  dihord4  42507  dihord5apre  42511  pellex  44035  jm2.27  44208