Theorem simp12r 1304

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

Assertion

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

Proof of Theorem simp12r

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  ackbij1lem16  10205  lsmcv  21234  nllyrest  23604  axcontlem4  29226  eqlkr  39735  athgt  40092  llncvrlpln2  40193  4atlem11b  40244  2lnat  40420  cdlemblem  40429  pclfinN  40536  lhp2at0nle  40671  4atexlemex6  40710  cdlemd2  40835  cdlemd8  40841  cdleme15a  40910  cdleme16b  40915  cdleme16c  40916  cdleme16d  40917  cdleme20h  40952  cdleme21c  40963  cdleme21ct  40965  cdleme22cN  40978  cdleme23b  40986  cdleme26fALTN  40998  cdleme26f  40999  cdleme26f2ALTN  41000  cdleme26f2  41001  cdleme32le  41083  cdleme35f  41090  cdlemf1  41197  trlord  41205  cdlemg7aN  41261  cdlemg33c0  41338  trlcone  41364  cdlemg44  41369  cdlemg48  41373  cdlemky  41562  cdlemk11ta  41565  cdleml4N  41615  dihmeetlem3N  41941  dihmeetlem13N  41955  mapdpglem32  42341  baerlem3lem2  42346  baerlem5alem2  42347  baerlem5blem2  42348  mzpcong  43561  iscnrm3rlem8  49576