Theorem simp3lr 1242

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

Assertion

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

Proof of Theorem simp3lr

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  f1oiso2  7366  omeu  8617  ntrivcvgmul  15908  tsmsxp  24153  tgqioo  24810  ovolunlem2  25521  plyadd  26247  plymul  26248  coeeu  26255  nosupbnd1lem2  27742  noinfbnd1lem2  27757  tghilberti2  28568  btwnconn1lem2  35914  btwnconn1lem3  35915  btwnconn1lem4  35916  athgt  39157  2llnjN  39268  4atlem12b  39312  lncmp  39484  cdlema2N  39493  cdleme21ct  40030  cdleme24  40053  cdleme27a  40068  cdleme28  40074  cdleme42b  40179  cdlemf  40264  dihlsscpre  40935  dihord4  40959  dihord5apre  40963  pellex  42510  jm2.27  42684