Theorem simp12r 1306

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

Assertion

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

Proof of Theorem simp12r

Step	Hyp	Ref	Expression
1		simp2r 1219	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant1 1151	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:  ackbij1lem16  10342  lsmcv  21452  nllyrest  23838  axcontlem4  29578  eqlkr  40359  athgt  40716  llncvrlpln2  40817  4atlem11b  40868  2lnat  41044  cdlemblem  41053  pclfinN  41160  lhp2at0nle  41295  4atexlemex6  41334  cdlemd2  41459  cdlemd8  41465  cdleme15a  41534  cdleme16b  41539  cdleme16c  41540  cdleme16d  41541  cdleme20h  41576  cdleme21c  41587  cdleme21ct  41589  cdleme22cN  41602  cdleme23b  41610  cdleme26fALTN  41622  cdleme26f  41623  cdleme26f2ALTN  41624  cdleme26f2  41625  cdleme32le  41707  cdleme35f  41714  cdlemf1  41821  trlord  41829  cdlemg7aN  41885  cdlemg33c0  41962  trlcone  41988  cdlemg44  41993  cdlemg48  41997  cdlemky  42186  cdlemk11ta  42189  cdleml4N  42239  dihmeetlem3N  42565  dihmeetlem13N  42579  mapdpglem32  42965  baerlem3lem2  42970  baerlem5alem2  42971  baerlem5blem2  42972  mzpcong  44183  iscnrm3rlem8  50276