Theorem simp12r 1285

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

Assertion

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

Proof of Theorem simp12r

Step	Hyp	Ref	Expression
1		simp2r 1198	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant1 1131	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓)

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  ackbij1lem16  9975  lsmcv  20384  nllyrest  22618  axcontlem4  27316  eqlkr  37092  athgt  37449  llncvrlpln2  37550  4atlem11b  37601  2lnat  37777  cdlemblem  37786  pclfinN  37893  lhp2at0nle  38028  4atexlemex6  38067  cdlemd2  38192  cdlemd8  38198  cdleme15a  38267  cdleme16b  38272  cdleme16c  38273  cdleme16d  38274  cdleme20h  38309  cdleme21c  38320  cdleme21ct  38322  cdleme22cN  38335  cdleme23b  38343  cdleme26fALTN  38355  cdleme26f  38356  cdleme26f2ALTN  38357  cdleme26f2  38358  cdleme32le  38440  cdleme35f  38447  cdlemf1  38554  trlord  38562  cdlemg7aN  38618  cdlemg33c0  38695  trlcone  38721  cdlemg44  38726  cdlemg48  38730  cdlemky  38919  cdlemk11ta  38922  cdleml4N  38972  dihmeetlem3N  39298  dihmeetlem13N  39312  mapdpglem32  39698  baerlem3lem2  39703  baerlem5alem2  39704  baerlem5blem2  39705  mzpcong  40774  iscnrm3rlem8  46193