Theorem simp3rr 1245

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

Assertion

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

Proof of Theorem simp3rr

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

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

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

This theorem is referenced by:  omeu  8392  ntrivcvgmul  15595  tsmsxp  23287  tgqioo  23944  ovolunlem2  24643  plyadd  25359  plymul  25360  coeeu  25367  tghilberti2  26980  cvmlift2lem10  33253  nosupbnd1lem2  33891  noinfbnd1lem2  33906  btwnconn1lem1  34368  lplnexllnN  37557  2llnjN  37560  4atlem12b  37604  lplncvrlvol2  37608  lncmp  37776  cdlema2N  37785  cdleme11a  38253  cdleme24  38345  cdleme28  38366  cdlemefr29bpre0N  38399  cdlemefr29clN  38400  cdlemefr32fvaN  38402  cdlemefr32fva1  38403  cdlemefs29bpre0N  38409  cdlemefs29bpre1N  38410  cdlemefs29cpre1N  38411  cdlemefs29clN  38412  cdlemefs32fvaN  38415  cdlemefs32fva1  38416  cdleme36m  38454  cdleme17d3  38489  cdlemg36  38707  cdlemj3  38816  cdlemkid1  38915  cdlemk19ylem  38923  cdlemk19xlem  38935  dihlsscpre  39227  dihord4  39251  dihmeetlem1N  39283  dihatlat  39327  jm2.27  40810