Theorem simp3rr 1248

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

Assertion

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

Proof of Theorem simp3rr

Step	Hyp	Ref	Expression
1		simprr 772	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant3 1135	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  8129  omeu  8549  ntrivcvgmul  15868  tsmsxp  24042  tgqioo  24688  ovolunlem2  25399  plyadd  26122  plymul  26123  coeeu  26130  nosupbnd1lem2  27621  noinfbnd1lem2  27636  tghilberti2  28565  cvmlift2lem10  35299  btwnconn1lem1  36075  lplnexllnN  39558  2llnjN  39561  4atlem12b  39605  lplncvrlvol2  39609  lncmp  39777  cdlema2N  39786  cdleme11a  40254  cdleme24  40346  cdleme28  40367  cdlemefr29bpre0N  40400  cdlemefr29clN  40401  cdlemefr32fvaN  40403  cdlemefr32fva1  40404  cdlemefs29bpre0N  40410  cdlemefs29bpre1N  40411  cdlemefs29cpre1N  40412  cdlemefs29clN  40413  cdlemefs32fvaN  40416  cdlemefs32fva1  40417  cdleme36m  40455  cdleme17d3  40490  cdlemg36  40708  cdlemj3  40817  cdlemkid1  40916  cdlemk19ylem  40924  cdlemk19xlem  40936  dihlsscpre  41228  dihord4  41252  dihmeetlem1N  41284  dihatlat  41328  jm2.27  42997