Theorem simp3lr 1312

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

Assertion

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

Proof of Theorem simp3lr

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  f1oiso2  6765  omeu  7834  ntrivcvgmul  14833  tsmsxp  22159  tgqioo  22804  ovolunlem2  23466  plyadd  24172  plymul  24173  coeeu  24180  tghilberti2  25732  nosupbnd1lem2  32161  btwnconn1lem2  32501  btwnconn1lem3  32502  btwnconn1lem4  32503  athgt  35245  2llnjN  35356  4atlem12b  35400  lncmp  35572  cdlema2N  35581  cdleme21ct  36119  cdleme24  36142  cdleme27a  36157  cdleme28  36163  cdleme42b  36268  cdlemf  36353  dihlsscpre  37025  dihord4  37049  dihord5apre  37053  pellex  37901  jm2.27  38077