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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ackbij1lem16  10236  lsmcv  21302  nllyrest  23680  axcontlem4  29354  eqlkr  39914  athgt  40271  llncvrlpln2  40372  4atlem11b  40423  2lnat  40599  cdlemblem  40608  pclfinN  40715  lhp2at0nle  40850  4atexlemex6  40889  cdlemd2  41014  cdlemd8  41020  cdleme15a  41089  cdleme16b  41094  cdleme16c  41095  cdleme16d  41096  cdleme20h  41131  cdleme21c  41142  cdleme21ct  41144  cdleme22cN  41157  cdleme23b  41165  cdleme26fALTN  41177  cdleme26f  41178  cdleme26f2ALTN  41179  cdleme26f2  41180  cdleme32le  41262  cdleme35f  41269  cdlemf1  41376  trlord  41384  cdlemg7aN  41440  cdlemg33c0  41517  trlcone  41543  cdlemg44  41548  cdlemg48  41552  cdlemky  41741  cdlemk11ta  41744  cdleml4N  41794  dihmeetlem3N  42120  dihmeetlem13N  42134  mapdpglem32  42520  baerlem3lem2  42525  baerlem5alem2  42526  baerlem5blem2  42527  mzpcong  43740  iscnrm3rlem8  49766