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 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  ackbij1lem16  10230  lsmcv  20754  nllyrest  22990  axcontlem4  28225  eqlkr  37969  athgt  38327  llncvrlpln2  38428  4atlem11b  38479  2lnat  38655  cdlemblem  38664  pclfinN  38771  lhp2at0nle  38906  4atexlemex6  38945  cdlemd2  39070  cdlemd8  39076  cdleme15a  39145  cdleme16b  39150  cdleme16c  39151  cdleme16d  39152  cdleme20h  39187  cdleme21c  39198  cdleme21ct  39200  cdleme22cN  39213  cdleme23b  39221  cdleme26fALTN  39233  cdleme26f  39234  cdleme26f2ALTN  39235  cdleme26f2  39236  cdleme32le  39318  cdleme35f  39325  cdlemf1  39432  trlord  39440  cdlemg7aN  39496  cdlemg33c0  39573  trlcone  39599  cdlemg44  39604  cdlemg48  39608  cdlemky  39797  cdlemk11ta  39800  cdleml4N  39850  dihmeetlem3N  40176  dihmeetlem13N  40190  mapdpglem32  40576  baerlem3lem2  40581  baerlem5alem2  40582  baerlem5blem2  40583  mzpcong  41711  iscnrm3rlem8  47580