Theorem simp12r 1289

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

Assertion

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

Proof of Theorem simp12r

Step	Hyp	Ref	Expression
1		simp2r 1202	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant1 1134	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:  ackbij1lem16  10158  lsmcv  21113  nllyrest  23447  axcontlem4  29058  eqlkr  39504  athgt  39861  llncvrlpln2  39962  4atlem11b  40013  2lnat  40189  cdlemblem  40198  pclfinN  40305  lhp2at0nle  40440  4atexlemex6  40479  cdlemd2  40604  cdlemd8  40610  cdleme15a  40679  cdleme16b  40684  cdleme16c  40685  cdleme16d  40686  cdleme20h  40721  cdleme21c  40732  cdleme21ct  40734  cdleme22cN  40747  cdleme23b  40755  cdleme26fALTN  40767  cdleme26f  40768  cdleme26f2ALTN  40769  cdleme26f2  40770  cdleme32le  40852  cdleme35f  40859  cdlemf1  40966  trlord  40974  cdlemg7aN  41030  cdlemg33c0  41107  trlcone  41133  cdlemg44  41138  cdlemg48  41142  cdlemky  41331  cdlemk11ta  41334  cdleml4N  41384  dihmeetlem3N  41710  dihmeetlem13N  41724  mapdpglem32  42110  baerlem3lem2  42115  baerlem5alem2  42116  baerlem5blem2  42117  mzpcong  43358  iscnrm3rlem8  49335