Theorem simp12r 1287

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

Assertion

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

Proof of Theorem simp12r

Step	Hyp	Ref	Expression
1		simp2r 1200	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant1 1133	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  10303  lsmcv  21166  nllyrest  23515  axcontlem4  29000  eqlkr  39055  athgt  39413  llncvrlpln2  39514  4atlem11b  39565  2lnat  39741  cdlemblem  39750  pclfinN  39857  lhp2at0nle  39992  4atexlemex6  40031  cdlemd2  40156  cdlemd8  40162  cdleme15a  40231  cdleme16b  40236  cdleme16c  40237  cdleme16d  40238  cdleme20h  40273  cdleme21c  40284  cdleme21ct  40286  cdleme22cN  40299  cdleme23b  40307  cdleme26fALTN  40319  cdleme26f  40320  cdleme26f2ALTN  40321  cdleme26f2  40322  cdleme32le  40404  cdleme35f  40411  cdlemf1  40518  trlord  40526  cdlemg7aN  40582  cdlemg33c0  40659  trlcone  40685  cdlemg44  40690  cdlemg48  40694  cdlemky  40883  cdlemk11ta  40886  cdleml4N  40936  dihmeetlem3N  41262  dihmeetlem13N  41276  mapdpglem32  41662  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  mzpcong  42929  iscnrm3rlem8  48627