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  7360  omeu  8596  ntrivcvgmul  16076  tsmsxp  24479  tgqioo  25124  ovolunlem2  25824  plyadd  26541  plymul  26542  coeeu  26549  nosupbnd1lem2  28071  noinfbnd1lem2  28086  tghilberti2  29111  btwnconn1lem2  36945  btwnconn1lem3  36946  btwnconn1lem4  36947  athgt  40606  2llnjN  40717  4atlem12b  40761  lncmp  40933  cdlema2N  40942  cdleme21ct  41479  cdleme24  41502  cdleme27a  41517  cdleme28  41523  cdleme42b  41628  cdlemf  41713  dihlsscpre  42384  dihord4  42408  dihord5apre  42412  pellex  43935  jm2.27  44108