Theorem simp12r 1294

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

Assertion

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

Proof of Theorem simp12r

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ackbij1lem16  10154  lsmcv  21141  nllyrest  23476  axcontlem4  29061  eqlkr  39598  athgt  39955  llncvrlpln2  40056  4atlem11b  40107  2lnat  40283  cdlemblem  40292  pclfinN  40399  lhp2at0nle  40534  4atexlemex6  40573  cdlemd2  40698  cdlemd8  40704  cdleme15a  40773  cdleme16b  40778  cdleme16c  40779  cdleme16d  40780  cdleme20h  40815  cdleme21c  40826  cdleme21ct  40828  cdleme22cN  40841  cdleme23b  40849  cdleme26fALTN  40861  cdleme26f  40862  cdleme26f2ALTN  40863  cdleme26f2  40864  cdleme32le  40946  cdleme35f  40953  cdlemf1  41060  trlord  41068  cdlemg7aN  41124  cdlemg33c0  41201  trlcone  41227  cdlemg44  41232  cdlemg48  41236  cdlemky  41425  cdlemk11ta  41428  cdleml4N  41478  dihmeetlem3N  41804  dihmeetlem13N  41818  mapdpglem32  42204  baerlem3lem2  42209  baerlem5alem2  42210  baerlem5blem2  42211  mzpcong  43424  iscnrm3rlem8  49444