Theorem simp12r 1284

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

Assertion

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

Proof of Theorem simp12r

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  ackbij1lem16  9646  lsmcv  19906  nllyrest  22091  axcontlem4  26761  eqlkr  36395  athgt  36752  llncvrlpln2  36853  4atlem11b  36904  2lnat  37080  cdlemblem  37089  pclfinN  37196  lhp2at0nle  37331  4atexlemex6  37370  cdlemd2  37495  cdlemd8  37501  cdleme15a  37570  cdleme16b  37575  cdleme16c  37576  cdleme16d  37577  cdleme20h  37612  cdleme21c  37623  cdleme21ct  37625  cdleme22cN  37638  cdleme23b  37646  cdleme26fALTN  37658  cdleme26f  37659  cdleme26f2ALTN  37660  cdleme26f2  37661  cdleme32le  37743  cdleme35f  37750  cdlemf1  37857  trlord  37865  cdlemg7aN  37921  cdlemg33c0  37998  trlcone  38024  cdlemg44  38029  cdlemg48  38033  cdlemky  38222  cdlemk11ta  38225  cdleml4N  38275  dihmeetlem3N  38601  dihmeetlem13N  38615  mapdpglem32  39001  baerlem3lem2  39006  baerlem5alem2  39007  baerlem5blem2  39008  mzpcong  39913