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

This theorem is referenced by:  poxp3  8173  omeu  8621  ntrivcvgmul  15934  tsmsxp  24178  tgqioo  24835  ovolunlem2  25546  plyadd  26270  plymul  26271  coeeu  26278  nosupbnd1lem2  27768  noinfbnd1lem2  27783  tghilberti2  28660  cvmlift2lem10  35296  btwnconn1lem1  36068  lplnexllnN  39546  2llnjN  39549  4atlem12b  39593  lplncvrlvol2  39597  lncmp  39765  cdlema2N  39774  cdleme11a  40242  cdleme24  40334  cdleme28  40355  cdlemefr29bpre0N  40388  cdlemefr29clN  40389  cdlemefr32fvaN  40391  cdlemefr32fva1  40392  cdlemefs29bpre0N  40398  cdlemefs29bpre1N  40399  cdlemefs29cpre1N  40400  cdlemefs29clN  40401  cdlemefs32fvaN  40404  cdlemefs32fva1  40405  cdleme36m  40443  cdleme17d3  40478  cdlemg36  40696  cdlemj3  40805  cdlemkid1  40904  cdlemk19ylem  40912  cdlemk19xlem  40924  dihlsscpre  41216  dihord4  41240  dihmeetlem1N  41272  dihatlat  41316  jm2.27  42996