Theorem simp3rr 1249

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 1136	1 ⊢ ((𝜃 ∧ 𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓))) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  poxp3  8100  omeu  8520  ntrivcvgmul  15867  tsmsxp  24120  tgqioo  24765  ovolunlem2  25465  plyadd  26182  plymul  26183  coeeu  26190  nosupbnd1lem2  27673  noinfbnd1lem2  27688  tghilberti2  28706  cvmlift2lem10  35494  btwnconn1lem1  36269  lplnexllnN  40010  2llnjN  40013  4atlem12b  40057  lplncvrlvol2  40061  lncmp  40229  cdlema2N  40238  cdleme11a  40706  cdleme24  40798  cdleme28  40819  cdlemefr29bpre0N  40852  cdlemefr29clN  40853  cdlemefr32fvaN  40855  cdlemefr32fva1  40856  cdlemefs29bpre0N  40862  cdlemefs29bpre1N  40863  cdlemefs29cpre1N  40864  cdlemefs29clN  40865  cdlemefs32fvaN  40868  cdlemefs32fva1  40869  cdleme36m  40907  cdleme17d3  40942  cdlemg36  41160  cdlemj3  41269  cdlemkid1  41368  cdlemk19ylem  41376  cdlemk19xlem  41388  dihlsscpre  41680  dihord4  41704  dihmeetlem1N  41736  dihatlat  41780  jm2.27  43436