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  8194  omeu  8621  ntrivcvgmul  16100  tsmsxp  24504  tgqioo  25149  ovolunlem2  25849  plyadd  26566  plymul  26567  coeeu  26574  nosupbnd1lem2  28096  noinfbnd1lem2  28111  tghilberti2  29136  cvmlift2lem10  36244  btwnconn1lem1  37030  lplnexllnN  40813  2llnjN  40816  4atlem12b  40860  lplncvrlvol2  40864  lncmp  41032  cdlema2N  41041  cdleme11a  41509  cdleme24  41601  cdleme28  41622  cdlemefr29bpre0N  41655  cdlemefr29clN  41656  cdlemefr32fvaN  41658  cdlemefr32fva1  41659  cdlemefs29bpre0N  41665  cdlemefs29bpre1N  41666  cdlemefs29cpre1N  41667  cdlemefs29clN  41668  cdlemefs32fvaN  41671  cdlemefs32fva1  41672  cdleme36m  41710  cdleme17d3  41745  cdlemg36  41963  cdlemj3  42072  cdlemkid1  42171  cdlemk19ylem  42179  cdlemk19xlem  42191  dihlsscpre  42483  dihord4  42507  dihmeetlem1N  42539  dihatlat  42583  jm2.27  44208