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 769	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓)
2	1	3ad2ant3 1134	1 ⊢ ((𝜃 ∧ 𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  f1oiso2  7372  omeu  8622  ntrivcvgmul  15935  tsmsxp  24179  tgqioo  24836  ovolunlem2  25547  plyadd  26271  plymul  26272  coeeu  26279  nosupbnd1lem2  27769  noinfbnd1lem2  27784  tghilberti2  28661  btwnconn1lem2  36070  btwnconn1lem3  36071  btwnconn1lem4  36072  athgt  39439  2llnjN  39550  4atlem12b  39594  lncmp  39766  cdlema2N  39775  cdleme21ct  40312  cdleme24  40335  cdleme27a  40350  cdleme28  40356  cdleme42b  40461  cdlemf  40546  dihlsscpre  41217  dihord4  41241  dihord5apre  41245  pellex  42823  jm2.27  42997