Theorem simp3lr 1252

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

Assertion

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

Proof of Theorem simp3lr

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

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

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

This theorem is referenced by:  f1oiso2  7303  omeu  8517  ntrivcvgmul  15865  tsmsxp  24145  tgqioo  24790  ovolunlem2  25490  plyadd  26207  plymul  26208  coeeu  26215  nosupbnd1lem2  27698  noinfbnd1lem2  27713  tghilberti2  28731  btwnconn1lem2  36323  btwnconn1lem3  36324  btwnconn1lem4  36325  athgt  39955  2llnjN  40066  4atlem12b  40110  lncmp  40282  cdlema2N  40291  cdleme21ct  40828  cdleme24  40851  cdleme27a  40866  cdleme28  40872  cdleme42b  40977  cdlemf  41062  dihlsscpre  41733  dihord4  41757  dihord5apre  41761  pellex  43287  jm2.27  43460