Theorem simp3rr 1247

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

Assertion

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

Proof of Theorem simp3rr

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ 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 206  df-an 398  df-3an 1089

This theorem is referenced by:  omeu  8447  ntrivcvgmul  15659  tsmsxp  23351  tgqioo  24008  ovolunlem2  24707  plyadd  25423  plymul  25424  coeeu  25431  tghilberti2  27044  cvmlift2lem10  33319  nosupbnd1lem2  33957  noinfbnd1lem2  33972  btwnconn1lem1  34434  lplnexllnN  37620  2llnjN  37623  4atlem12b  37667  lplncvrlvol2  37671  lncmp  37839  cdlema2N  37848  cdleme11a  38316  cdleme24  38408  cdleme28  38429  cdlemefr29bpre0N  38462  cdlemefr29clN  38463  cdlemefr32fvaN  38465  cdlemefr32fva1  38466  cdlemefs29bpre0N  38472  cdlemefs29bpre1N  38473  cdlemefs29cpre1N  38474  cdlemefs29clN  38475  cdlemefs32fvaN  38478  cdlemefs32fva1  38479  cdleme36m  38517  cdleme17d3  38552  cdlemg36  38770  cdlemj3  38879  cdlemkid1  38978  cdlemk19ylem  38986  cdlemk19xlem  38998  dihlsscpre  39290  dihord4  39314  dihmeetlem1N  39346  dihatlat  39390  jm2.27  40868