Theorem simp3rr 1266

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

Assertion

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

Proof of Theorem simp3rr

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp3  8169  omeu  8596  ntrivcvgmul  16076  tsmsxp  24479  tgqioo  25124  ovolunlem2  25824  plyadd  26541  plymul  26542  coeeu  26549  nosupbnd1lem2  28071  noinfbnd1lem2  28086  tghilberti2  29111  cvmlift2lem10  36163  btwnconn1lem1  36944  lplnexllnN  40714  2llnjN  40717  4atlem12b  40761  lplncvrlvol2  40765  lncmp  40933  cdlema2N  40942  cdleme11a  41410  cdleme24  41502  cdleme28  41523  cdlemefr29bpre0N  41556  cdlemefr29clN  41557  cdlemefr32fvaN  41559  cdlemefr32fva1  41560  cdlemefs29bpre0N  41566  cdlemefs29bpre1N  41567  cdlemefs29cpre1N  41568  cdlemefs29clN  41569  cdlemefs32fvaN  41572  cdlemefs32fva1  41573  cdleme36m  41611  cdleme17d3  41646  cdlemg36  41864  cdlemj3  41973  cdlemkid1  42072  cdlemk19ylem  42080  cdlemk19xlem  42092  dihlsscpre  42384  dihord4  42408  dihmeetlem1N  42440  dihatlat  42484  jm2.27  44108