Theorem simp3rr 1249

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

Assertion

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

Proof of Theorem simp3rr

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

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

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 1089

This theorem is referenced by:  poxp3  8093  omeu  8513  ntrivcvgmul  15858  tsmsxp  24130  tgqioo  24775  ovolunlem2  25475  plyadd  26192  plymul  26193  coeeu  26200  nosupbnd1lem2  27687  noinfbnd1lem2  27702  tghilberti2  28720  cvmlift2lem10  35510  btwnconn1lem1  36285  lplnexllnN  40024  2llnjN  40027  4atlem12b  40071  lplncvrlvol2  40075  lncmp  40243  cdlema2N  40252  cdleme11a  40720  cdleme24  40812  cdleme28  40833  cdlemefr29bpre0N  40866  cdlemefr29clN  40867  cdlemefr32fvaN  40869  cdlemefr32fva1  40870  cdlemefs29bpre0N  40876  cdlemefs29bpre1N  40877  cdlemefs29cpre1N  40878  cdlemefs29clN  40879  cdlemefs32fvaN  40882  cdlemefs32fva1  40883  cdleme36m  40921  cdleme17d3  40956  cdlemg36  41174  cdlemj3  41283  cdlemkid1  41382  cdlemk19ylem  41390  cdlemk19xlem  41402  dihlsscpre  41694  dihord4  41718  dihmeetlem1N  41750  dihatlat  41794  jm2.27  43454