Theorem simp12r 1283

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

Assertion

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

Proof of Theorem simp12r

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  ackbij1lem16  9651  lsmcv  19907  nllyrest  22088  axcontlem4  26747  eqlkr  36229  athgt  36586  llncvrlpln2  36687  4atlem11b  36738  2lnat  36914  cdlemblem  36923  pclfinN  37030  lhp2at0nle  37165  4atexlemex6  37204  cdlemd2  37329  cdlemd8  37335  cdleme15a  37404  cdleme16b  37409  cdleme16c  37410  cdleme16d  37411  cdleme20h  37446  cdleme21c  37457  cdleme21ct  37459  cdleme22cN  37472  cdleme23b  37480  cdleme26fALTN  37492  cdleme26f  37493  cdleme26f2ALTN  37494  cdleme26f2  37495  cdleme32le  37577  cdleme35f  37584  cdlemf1  37691  trlord  37699  cdlemg7aN  37755  cdlemg33c0  37832  trlcone  37858  cdlemg44  37863  cdlemg48  37867  cdlemky  38056  cdlemk11ta  38059  cdleml4N  38109  dihmeetlem3N  38435  dihmeetlem13N  38449  mapdpglem32  38835  baerlem3lem2  38840  baerlem5alem2  38841  baerlem5blem2  38842  mzpcong  39562