Theorem simp3lr 1244

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

Assertion

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

Proof of Theorem simp3lr

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  f1oiso2  7223  omeu  8416  ntrivcvgmul  15614  tsmsxp  23306  tgqioo  23963  ovolunlem2  24662  plyadd  25378  plymul  25379  coeeu  25386  tghilberti2  26999  nosupbnd1lem2  33912  noinfbnd1lem2  33927  btwnconn1lem2  34390  btwnconn1lem3  34391  btwnconn1lem4  34392  athgt  37470  2llnjN  37581  4atlem12b  37625  lncmp  37797  cdlema2N  37806  cdleme21ct  38343  cdleme24  38366  cdleme27a  38381  cdleme28  38387  cdleme42b  38492  cdlemf  38577  dihlsscpre  39248  dihord4  39272  dihord5apre  39276  pellex  40657  jm2.27  40830