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  10240  lsmcv  21334  nllyrest  23718  axcontlem4  29432  eqlkr  39980  athgt  40337  llncvrlpln2  40438  4atlem11b  40489  2lnat  40665  cdlemblem  40674  pclfinN  40781  lhp2at0nle  40916  4atexlemex6  40955  cdlemd2  41080  cdlemd8  41086  cdleme15a  41155  cdleme16b  41160  cdleme16c  41161  cdleme16d  41162  cdleme20h  41197  cdleme21c  41208  cdleme21ct  41210  cdleme22cN  41223  cdleme23b  41231  cdleme26fALTN  41243  cdleme26f  41244  cdleme26f2ALTN  41245  cdleme26f2  41246  cdleme32le  41328  cdleme35f  41335  cdlemf1  41442  trlord  41450  cdlemg7aN  41506  cdlemg33c0  41583  trlcone  41609  cdlemg44  41614  cdlemg48  41618  cdlemky  41807  cdlemk11ta  41810  cdleml4N  41860  dihmeetlem3N  42186  dihmeetlem13N  42200  mapdpglem32  42586  baerlem3lem2  42591  baerlem5alem2  42592  baerlem5blem2  42593  mzpcong  43821  iscnrm3rlem8  49881