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  8155  omeu  8579  ntrivcvgmul  15982  tsmsxp  24349  tgqioo  24994  ovolunlem2  25694  plyadd  26411  plymul  26412  coeeu  26419  nosupbnd1lem2  27910  noinfbnd1lem2  27925  tghilberti2  28948  cvmlift2lem10  35825  btwnconn1lem1  36600  lplnexllnN  40379  2llnjN  40382  4atlem12b  40426  lplncvrlvol2  40430  lncmp  40598  cdlema2N  40607  cdleme11a  41075  cdleme24  41167  cdleme28  41188  cdlemefr29bpre0N  41221  cdlemefr29clN  41222  cdlemefr32fvaN  41224  cdlemefr32fva1  41225  cdlemefs29bpre0N  41231  cdlemefs29bpre1N  41232  cdlemefs29cpre1N  41233  cdlemefs29clN  41234  cdlemefs32fvaN  41237  cdlemefs32fva1  41238  cdleme36m  41276  cdleme17d3  41311  cdlemg36  41529  cdlemj3  41638  cdlemkid1  41737  cdlemk19ylem  41745  cdlemk19xlem  41757  dihlsscpre  42049  dihord4  42073  dihmeetlem1N  42105  dihatlat  42149  jm2.27  43776