Theorem simp12r 1392

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

Assertion

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

Proof of Theorem simp12r

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  ackbij1lem16  9371  lsmcv  19500  nllyrest  21659  axcontlem4  26265  eqlkr  35173  athgt  35530  llncvrlpln2  35631  4atlem11b  35682  2lnat  35858  cdlemblem  35867  pclfinN  35974  lhp2at0nle  36109  4atexlemex6  36148  cdlemd2  36273  cdlemd8  36279  cdleme15a  36348  cdleme16b  36353  cdleme16c  36354  cdleme16d  36355  cdleme20h  36390  cdleme21c  36401  cdleme21ct  36403  cdleme22cN  36416  cdleme23b  36424  cdleme26fALTN  36436  cdleme26f  36437  cdleme26f2ALTN  36438  cdleme26f2  36439  cdleme32le  36521  cdleme35f  36528  cdlemf1  36635  trlord  36643  cdlemg7aN  36699  cdlemg33c0  36776  trlcone  36802  cdlemg44  36807  cdlemg48  36811  cdlemky  37000  cdlemk11ta  37003  cdleml4N  37053  dihmeetlem3N  37379  dihmeetlem13N  37393  mapdpglem32  37779  baerlem3lem2  37784  baerlem5alem2  37785  baerlem5blem2  37786  mzpcong  38381