Theorem simp3lr 1255

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

Assertion

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

Proof of Theorem simp3lr

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095

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 399  df-3an 1097

This theorem is referenced by:  f1oiso2  7321  omeu  8538  ntrivcvgmul  15904  tsmsxp  24184  tgqioo  24829  ovolunlem2  25529  plyadd  26246  plymul  26247  coeeu  26254  nosupbnd1lem2  27739  noinfbnd1lem2  27754  tghilberti2  28773  btwnconn1lem2  36376  btwnconn1lem3  36377  btwnconn1lem4  36378  athgt  40018  2llnjN  40129  4atlem12b  40173  lncmp  40345  cdlema2N  40354  cdleme21ct  40891  cdleme24  40914  cdleme27a  40929  cdleme28  40935  cdleme42b  41040  cdlemf  41125  dihlsscpre  41796  dihord4  41820  dihord5apre  41824  pellex  43350  jm2.27  43523