Theorem simp3rr 1128

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

Assertion

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

Proof of Theorem simp3rr

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  omeu  7552  ntrivcvgmul  14473  tsmsxp  21768  tgqioo  22411  ovolunlem2  23073  plyadd  23777  plymul  23778  coeeu  23785  tghilberti2  25333  cvmlift2lem10  30548  btwnconn1lem1  31364  lplnexllnN  33868  2llnjN  33871  4atlem12b  33915  lplncvrlvol2  33919  lncmp  34087  cdlema2N  34096  cdleme11a  34565  cdleme24  34658  cdleme28  34679  cdlemefr29bpre0N  34712  cdlemefr29clN  34713  cdlemefr32fvaN  34715  cdlemefr32fva1  34716  cdlemefs29bpre0N  34722  cdlemefs29bpre1N  34723  cdlemefs29cpre1N  34724  cdlemefs29clN  34725  cdlemefs32fvaN  34728  cdlemefs32fva1  34729  cdleme36m  34767  cdleme17d3  34802  cdlemg36  35020  cdlemj3  35129  cdlemkid1  35228  cdlemk19ylem  35236  cdlemk19xlem  35248  dihlsscpre  35541  dihord4  35565  dihmeetlem1N  35597  dihatlat  35641  jm2.27  36593