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 785	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant3 1153	1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp3  8152  omeu  8576  ntrivcvgmul  15995  tsmsxp  24387  tgqioo  25032  ovolunlem2  25732  plyadd  26450  plymul  26451  coeeu  26458  nosupbnd1lem2  27953  noinfbnd1lem2  27968  tghilberti2  28993  cvmlift2lem10  35899  btwnconn1lem1  36675  lplnexllnN  40445  2llnjN  40448  4atlem12b  40492  lplncvrlvol2  40496  lncmp  40664  cdlema2N  40673  cdleme11a  41141  cdleme24  41233  cdleme28  41254  cdlemefr29bpre0N  41287  cdlemefr29clN  41288  cdlemefr32fvaN  41290  cdlemefr32fva1  41291  cdlemefs29bpre0N  41297  cdlemefs29bpre1N  41298  cdlemefs29cpre1N  41299  cdlemefs29clN  41300  cdlemefs32fvaN  41303  cdlemefs32fva1  41304  cdleme36m  41342  cdleme17d3  41377  cdlemg36  41595  cdlemj3  41704  cdlemkid1  41803  cdlemk19ylem  41811  cdlemk19xlem  41823  dihlsscpre  42115  dihord4  42139  dihmeetlem1N  42171  dihatlat  42215  jm2.27  43857