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  10125  lsmcv  21079  nllyrest  23402  axcontlem4  28946  eqlkr  39144  athgt  39501  llncvrlpln2  39602  4atlem11b  39653  2lnat  39829  cdlemblem  39838  pclfinN  39945  lhp2at0nle  40080  4atexlemex6  40119  cdlemd2  40244  cdlemd8  40250  cdleme15a  40319  cdleme16b  40324  cdleme16c  40325  cdleme16d  40326  cdleme20h  40361  cdleme21c  40372  cdleme21ct  40374  cdleme22cN  40387  cdleme23b  40395  cdleme26fALTN  40407  cdleme26f  40408  cdleme26f2ALTN  40409  cdleme26f2  40410  cdleme32le  40492  cdleme35f  40499  cdlemf1  40606  trlord  40614  cdlemg7aN  40670  cdlemg33c0  40747  trlcone  40773  cdlemg44  40778  cdlemg48  40782  cdlemky  40971  cdlemk11ta  40974  cdleml4N  41024  dihmeetlem3N  41350  dihmeetlem13N  41364  mapdpglem32  41750  baerlem3lem2  41755  baerlem5alem2  41756  baerlem5blem2  41757  mzpcong  43011  iscnrm3rlem8  48984