Theorem simp12r 1282

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

Assertion

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

Proof of Theorem simp12r

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

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

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 1084

This theorem is referenced by:  ackbij1lem16  9649  lsmcv  19905  nllyrest  22086  axcontlem4  26745  eqlkr  36227  athgt  36584  llncvrlpln2  36685  4atlem11b  36736  2lnat  36912  cdlemblem  36921  pclfinN  37028  lhp2at0nle  37163  4atexlemex6  37202  cdlemd2  37327  cdlemd8  37333  cdleme15a  37402  cdleme16b  37407  cdleme16c  37408  cdleme16d  37409  cdleme20h  37444  cdleme21c  37455  cdleme21ct  37457  cdleme22cN  37470  cdleme23b  37478  cdleme26fALTN  37490  cdleme26f  37491  cdleme26f2ALTN  37492  cdleme26f2  37493  cdleme32le  37575  cdleme35f  37582  cdlemf1  37689  trlord  37697  cdlemg7aN  37753  cdlemg33c0  37830  trlcone  37856  cdlemg44  37861  cdlemg48  37865  cdlemky  38054  cdlemk11ta  38057  cdleml4N  38107  dihmeetlem3N  38433  dihmeetlem13N  38447  mapdpglem32  38833  baerlem3lem2  38838  baerlem5alem2  38839  baerlem5blem2  38840  mzpcong  39559