Theorem simp3lr 1247

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

Assertion

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

Proof of Theorem simp3lr

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  f1oiso2  7307  omeu  8520  ntrivcvgmul  15867  tsmsxp  24120  tgqioo  24765  ovolunlem2  25465  plyadd  26182  plymul  26183  coeeu  26190  nosupbnd1lem2  27673  noinfbnd1lem2  27688  tghilberti2  28706  btwnconn1lem2  36270  btwnconn1lem3  36271  btwnconn1lem4  36272  athgt  39902  2llnjN  40013  4atlem12b  40057  lncmp  40229  cdlema2N  40238  cdleme21ct  40775  cdleme24  40798  cdleme27a  40813  cdleme28  40819  cdleme42b  40924  cdlemf  41009  dihlsscpre  41680  dihord4  41704  dihord5apre  41708  pellex  43263  jm2.27  43436