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  10248  lsmcv  21102  nllyrest  23424  axcontlem4  28946  eqlkr  39117  athgt  39475  llncvrlpln2  39576  4atlem11b  39627  2lnat  39803  cdlemblem  39812  pclfinN  39919  lhp2at0nle  40054  4atexlemex6  40093  cdlemd2  40218  cdlemd8  40224  cdleme15a  40293  cdleme16b  40298  cdleme16c  40299  cdleme16d  40300  cdleme20h  40335  cdleme21c  40346  cdleme21ct  40348  cdleme22cN  40361  cdleme23b  40369  cdleme26fALTN  40381  cdleme26f  40382  cdleme26f2ALTN  40383  cdleme26f2  40384  cdleme32le  40466  cdleme35f  40473  cdlemf1  40580  trlord  40588  cdlemg7aN  40644  cdlemg33c0  40721  trlcone  40747  cdlemg44  40752  cdlemg48  40756  cdlemky  40945  cdlemk11ta  40948  cdleml4N  40998  dihmeetlem3N  41324  dihmeetlem13N  41338  mapdpglem32  41724  baerlem3lem2  41729  baerlem5alem2  41730  baerlem5blem2  41731  mzpcong  42996  iscnrm3rlem8  48921