Theorem simp3rr 1243

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

Assertion

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

Proof of Theorem simp3rr

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  omeu  8211  ntrivcvgmul  15258  tsmsxp  22763  tgqioo  23408  ovolunlem2  24099  plyadd  24807  plymul  24808  coeeu  24815  tghilberti2  26424  cvmlift2lem10  32559  nosupbnd1lem2  33209  btwnconn1lem1  33548  lplnexllnN  36715  2llnjN  36718  4atlem12b  36762  lplncvrlvol2  36766  lncmp  36934  cdlema2N  36943  cdleme11a  37411  cdleme24  37503  cdleme28  37524  cdlemefr29bpre0N  37557  cdlemefr29clN  37558  cdlemefr32fvaN  37560  cdlemefr32fva1  37561  cdlemefs29bpre0N  37567  cdlemefs29bpre1N  37568  cdlemefs29cpre1N  37569  cdlemefs29clN  37570  cdlemefs32fvaN  37573  cdlemefs32fva1  37574  cdleme36m  37612  cdleme17d3  37647  cdlemg36  37865  cdlemj3  37974  cdlemkid1  38073  cdlemk19ylem  38081  cdlemk19xlem  38093  dihlsscpre  38385  dihord4  38409  dihmeetlem1N  38441  dihatlat  38485  jm2.27  39625