Theorem simp3rr 1246

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

Assertion

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

Proof of Theorem simp3rr

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

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

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 396  df-3an 1088

This theorem is referenced by:  poxp3  8140  omeu  8589  ntrivcvgmul  15853  tsmsxp  23880  tgqioo  24537  ovolunlem2  25248  plyadd  25967  plymul  25968  coeeu  25975  nosupbnd1lem2  27449  noinfbnd1lem2  27464  tghilberti2  28157  cvmlift2lem10  34602  btwnconn1lem1  35364  lplnexllnN  38739  2llnjN  38742  4atlem12b  38786  lplncvrlvol2  38790  lncmp  38958  cdlema2N  38967  cdleme11a  39435  cdleme24  39527  cdleme28  39548  cdlemefr29bpre0N  39581  cdlemefr29clN  39582  cdlemefr32fvaN  39584  cdlemefr32fva1  39585  cdlemefs29bpre0N  39591  cdlemefs29bpre1N  39592  cdlemefs29cpre1N  39593  cdlemefs29clN  39594  cdlemefs32fvaN  39597  cdlemefs32fva1  39598  cdleme36m  39636  cdleme17d3  39671  cdlemg36  39889  cdlemj3  39998  cdlemkid1  40097  cdlemk19ylem  40105  cdlemk19xlem  40117  dihlsscpre  40409  dihord4  40433  dihmeetlem1N  40465  dihatlat  40509  jm2.27  42050