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 1134	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓)

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

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 1089

This theorem is referenced by:  ackbij1lem16  10274  lsmcv  21143  nllyrest  23494  axcontlem4  28982  eqlkr  39100  athgt  39458  llncvrlpln2  39559  4atlem11b  39610  2lnat  39786  cdlemblem  39795  pclfinN  39902  lhp2at0nle  40037  4atexlemex6  40076  cdlemd2  40201  cdlemd8  40207  cdleme15a  40276  cdleme16b  40281  cdleme16c  40282  cdleme16d  40283  cdleme20h  40318  cdleme21c  40329  cdleme21ct  40331  cdleme22cN  40344  cdleme23b  40352  cdleme26fALTN  40364  cdleme26f  40365  cdleme26f2ALTN  40366  cdleme26f2  40367  cdleme32le  40449  cdleme35f  40456  cdlemf1  40563  trlord  40571  cdlemg7aN  40627  cdlemg33c0  40704  trlcone  40730  cdlemg44  40735  cdlemg48  40739  cdlemky  40928  cdlemk11ta  40931  cdleml4N  40981  dihmeetlem3N  41307  dihmeetlem13N  41321  mapdpglem32  41707  baerlem3lem2  41712  baerlem5alem2  41713  baerlem5blem2  41714  mzpcong  42984  iscnrm3rlem8  48844