Theorem simp12r 1300

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

Assertion

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

Proof of Theorem simp12r

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

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

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  ackbij1lem16  10187  lsmcv  21191  nllyrest  23526  axcontlem4  29114  eqlkr  39687  athgt  40044  llncvrlpln2  40145  4atlem11b  40196  2lnat  40372  cdlemblem  40381  pclfinN  40488  lhp2at0nle  40623  4atexlemex6  40662  cdlemd2  40787  cdlemd8  40793  cdleme15a  40862  cdleme16b  40867  cdleme16c  40868  cdleme16d  40869  cdleme20h  40904  cdleme21c  40915  cdleme21ct  40917  cdleme22cN  40930  cdleme23b  40938  cdleme26fALTN  40950  cdleme26f  40951  cdleme26f2ALTN  40952  cdleme26f2  40953  cdleme32le  41035  cdleme35f  41042  cdlemf1  41149  trlord  41157  cdlemg7aN  41213  cdlemg33c0  41290  trlcone  41316  cdlemg44  41321  cdlemg48  41325  cdlemky  41514  cdlemk11ta  41517  cdleml4N  41567  dihmeetlem3N  41893  dihmeetlem13N  41907  mapdpglem32  42293  baerlem3lem2  42298  baerlem5alem2  42299  baerlem5blem2  42300  mzpcong  43513  iscnrm3rlem8  49532