Theorem simp3rr 1244

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

Assertion

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

Proof of Theorem simp3rr

Step	Hyp	Ref	Expression
1		simprr 771	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant3 1132	1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  poxp3  8161  omeu  8612  ntrivcvgmul  15888  tsmsxp  24079  tgqioo  24736  ovolunlem2  25447  plyadd  26171  plymul  26172  coeeu  26179  nosupbnd1lem2  27662  noinfbnd1lem2  27677  tghilberti2  28462  cvmlift2lem10  34955  btwnconn1lem1  35716  lplnexllnN  39069  2llnjN  39072  4atlem12b  39116  lplncvrlvol2  39120  lncmp  39288  cdlema2N  39297  cdleme11a  39765  cdleme24  39857  cdleme28  39878  cdlemefr29bpre0N  39911  cdlemefr29clN  39912  cdlemefr32fvaN  39914  cdlemefr32fva1  39915  cdlemefs29bpre0N  39921  cdlemefs29bpre1N  39922  cdlemefs29cpre1N  39923  cdlemefs29clN  39924  cdlemefs32fvaN  39927  cdlemefs32fva1  39928  cdleme36m  39966  cdleme17d3  40001  cdlemg36  40219  cdlemj3  40328  cdlemkid1  40427  cdlemk19ylem  40435  cdlemk19xlem  40447  dihlsscpre  40739  dihord4  40763  dihmeetlem1N  40795  dihatlat  40839  jm2.27  42460