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  10315  lsmcv  21424  nllyrest  23810  axcontlem4  29550  eqlkr  40249  athgt  40606  llncvrlpln2  40707  4atlem11b  40758  2lnat  40934  cdlemblem  40943  pclfinN  41050  lhp2at0nle  41185  4atexlemex6  41224  cdlemd2  41349  cdlemd8  41355  cdleme15a  41424  cdleme16b  41429  cdleme16c  41430  cdleme16d  41431  cdleme20h  41466  cdleme21c  41477  cdleme21ct  41479  cdleme22cN  41492  cdleme23b  41500  cdleme26fALTN  41512  cdleme26f  41513  cdleme26f2ALTN  41514  cdleme26f2  41515  cdleme32le  41597  cdleme35f  41604  cdlemf1  41711  trlord  41719  cdlemg7aN  41775  cdlemg33c0  41852  trlcone  41878  cdlemg44  41883  cdlemg48  41887  cdlemky  42076  cdlemk11ta  42079  cdleml4N  42129  dihmeetlem3N  42455  dihmeetlem13N  42469  mapdpglem32  42855  baerlem3lem2  42860  baerlem5alem2  42861  baerlem5blem2  42862  mzpcong  44072  iscnrm3rlem8  50154