Theorem simp12r 1288

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

Assertion

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

Proof of Theorem simp12r

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

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

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 1088

This theorem is referenced by:  ackbij1lem16  10144  lsmcv  21096  nllyrest  23430  axcontlem4  29040  eqlkr  39355  athgt  39712  llncvrlpln2  39813  4atlem11b  39864  2lnat  40040  cdlemblem  40049  pclfinN  40156  lhp2at0nle  40291  4atexlemex6  40330  cdlemd2  40455  cdlemd8  40461  cdleme15a  40530  cdleme16b  40535  cdleme16c  40536  cdleme16d  40537  cdleme20h  40572  cdleme21c  40583  cdleme21ct  40585  cdleme22cN  40598  cdleme23b  40606  cdleme26fALTN  40618  cdleme26f  40619  cdleme26f2ALTN  40620  cdleme26f2  40621  cdleme32le  40703  cdleme35f  40710  cdlemf1  40817  trlord  40825  cdlemg7aN  40881  cdlemg33c0  40958  trlcone  40984  cdlemg44  40989  cdlemg48  40993  cdlemky  41182  cdlemk11ta  41185  cdleml4N  41235  dihmeetlem3N  41561  dihmeetlem13N  41575  mapdpglem32  41961  baerlem3lem2  41966  baerlem5alem2  41967  baerlem5blem2  41968  mzpcong  43210  iscnrm3rlem8  49188