Theorem simp12r 1285

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

Assertion

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

Proof of Theorem simp12r

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  ackbij1lem16  10244  lsmcv  21011  nllyrest  23364  axcontlem4  28752  eqlkr  38495  athgt  38853  llncvrlpln2  38954  4atlem11b  39005  2lnat  39181  cdlemblem  39190  pclfinN  39297  lhp2at0nle  39432  4atexlemex6  39471  cdlemd2  39596  cdlemd8  39602  cdleme15a  39671  cdleme16b  39676  cdleme16c  39677  cdleme16d  39678  cdleme20h  39713  cdleme21c  39724  cdleme21ct  39726  cdleme22cN  39739  cdleme23b  39747  cdleme26fALTN  39759  cdleme26f  39760  cdleme26f2ALTN  39761  cdleme26f2  39762  cdleme32le  39844  cdleme35f  39851  cdlemf1  39958  trlord  39966  cdlemg7aN  40022  cdlemg33c0  40099  trlcone  40125  cdlemg44  40130  cdlemg48  40134  cdlemky  40323  cdlemk11ta  40326  cdleml4N  40376  dihmeetlem3N  40702  dihmeetlem13N  40716  mapdpglem32  41102  baerlem3lem2  41107  baerlem5alem2  41108  baerlem5blem2  41109  mzpcong  42305  iscnrm3rlem8  47879