Theorem simp3rr 1266

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

Assertion

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

Proof of Theorem simp3rr

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  poxp3  8147  omeu  8571  ntrivcvgmul  15958  tsmsxp  24293  tgqioo  24938  ovolunlem2  25638  plyadd  26355  plymul  26356  coeeu  26363  nosupbnd1lem2  27851  noinfbnd1lem2  27866  tghilberti2  28889  cvmlift2lem10  35782  btwnconn1lem1  36557  lplnexllnN  40316  2llnjN  40319  4atlem12b  40363  lplncvrlvol2  40367  lncmp  40535  cdlema2N  40544  cdleme11a  41012  cdleme24  41104  cdleme28  41125  cdlemefr29bpre0N  41158  cdlemefr29clN  41159  cdlemefr32fvaN  41161  cdlemefr32fva1  41162  cdlemefs29bpre0N  41168  cdlemefs29bpre1N  41169  cdlemefs29cpre1N  41170  cdlemefs29clN  41171  cdlemefs32fvaN  41174  cdlemefs32fva1  41175  cdleme36m  41213  cdleme17d3  41248  cdlemg36  41466  cdlemj3  41575  cdlemkid1  41674  cdlemk19ylem  41682  cdlemk19xlem  41694  dihlsscpre  41986  dihord4  42010  dihmeetlem1N  42042  dihatlat  42086  jm2.27  43715