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  10187  lsmcv  21051  nllyrest  23373  axcontlem4  28894  eqlkr  39092  athgt  39450  llncvrlpln2  39551  4atlem11b  39602  2lnat  39778  cdlemblem  39787  pclfinN  39894  lhp2at0nle  40029  4atexlemex6  40068  cdlemd2  40193  cdlemd8  40199  cdleme15a  40268  cdleme16b  40273  cdleme16c  40274  cdleme16d  40275  cdleme20h  40310  cdleme21c  40321  cdleme21ct  40323  cdleme22cN  40336  cdleme23b  40344  cdleme26fALTN  40356  cdleme26f  40357  cdleme26f2ALTN  40358  cdleme26f2  40359  cdleme32le  40441  cdleme35f  40448  cdlemf1  40555  trlord  40563  cdlemg7aN  40619  cdlemg33c0  40696  trlcone  40722  cdlemg44  40727  cdlemg48  40731  cdlemky  40920  cdlemk11ta  40923  cdleml4N  40973  dihmeetlem3N  41299  dihmeetlem13N  41313  mapdpglem32  41699  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  mzpcong  42961  iscnrm3rlem8  48935