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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  ackbij1lem16  10132  lsmcv  21080  nllyrest  23402  axcontlem4  28947  eqlkr  39219  athgt  39576  llncvrlpln2  39677  4atlem11b  39728  2lnat  39904  cdlemblem  39913  pclfinN  40020  lhp2at0nle  40155  4atexlemex6  40194  cdlemd2  40319  cdlemd8  40325  cdleme15a  40394  cdleme16b  40399  cdleme16c  40400  cdleme16d  40401  cdleme20h  40436  cdleme21c  40447  cdleme21ct  40449  cdleme22cN  40462  cdleme23b  40470  cdleme26fALTN  40482  cdleme26f  40483  cdleme26f2ALTN  40484  cdleme26f2  40485  cdleme32le  40567  cdleme35f  40574  cdlemf1  40681  trlord  40689  cdlemg7aN  40745  cdlemg33c0  40822  trlcone  40848  cdlemg44  40853  cdlemg48  40857  cdlemky  41046  cdlemk11ta  41049  cdleml4N  41099  dihmeetlem3N  41425  dihmeetlem13N  41439  mapdpglem32  41825  baerlem3lem2  41830  baerlem5alem2  41831  baerlem5blem2  41832  mzpcong  43090  iscnrm3rlem8  49072