Theorem simp12r 1306

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

Assertion

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

Proof of Theorem simp12r

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  ackbij1lem16  10218  lsmcv  21246  nllyrest  23624  axcontlem4  29298  eqlkr  39854  athgt  40211  llncvrlpln2  40312  4atlem11b  40363  2lnat  40539  cdlemblem  40548  pclfinN  40655  lhp2at0nle  40790  4atexlemex6  40829  cdlemd2  40954  cdlemd8  40960  cdleme15a  41029  cdleme16b  41034  cdleme16c  41035  cdleme16d  41036  cdleme20h  41071  cdleme21c  41082  cdleme21ct  41084  cdleme22cN  41097  cdleme23b  41105  cdleme26fALTN  41117  cdleme26f  41118  cdleme26f2ALTN  41119  cdleme26f2  41120  cdleme32le  41202  cdleme35f  41209  cdlemf1  41316  trlord  41324  cdlemg7aN  41380  cdlemg33c0  41457  trlcone  41483  cdlemg44  41488  cdlemg48  41492  cdlemky  41681  cdlemk11ta  41684  cdleml4N  41734  dihmeetlem3N  42060  dihmeetlem13N  42074  mapdpglem32  42460  baerlem3lem2  42465  baerlem5alem2  42466  baerlem5blem2  42467  mzpcong  43682  iscnrm3rlem8  49708