Theorem simp12r 1289

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

Assertion

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

Proof of Theorem simp12r

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  ackbij1lem16  10156  lsmcv  21139  nllyrest  23451  axcontlem4  29036  eqlkr  39545  athgt  39902  llncvrlpln2  40003  4atlem11b  40054  2lnat  40230  cdlemblem  40239  pclfinN  40346  lhp2at0nle  40481  4atexlemex6  40520  cdlemd2  40645  cdlemd8  40651  cdleme15a  40720  cdleme16b  40725  cdleme16c  40726  cdleme16d  40727  cdleme20h  40762  cdleme21c  40773  cdleme21ct  40775  cdleme22cN  40788  cdleme23b  40796  cdleme26fALTN  40808  cdleme26f  40809  cdleme26f2ALTN  40810  cdleme26f2  40811  cdleme32le  40893  cdleme35f  40900  cdlemf1  41007  trlord  41015  cdlemg7aN  41071  cdlemg33c0  41148  trlcone  41174  cdlemg44  41179  cdlemg48  41183  cdlemky  41372  cdlemk11ta  41375  cdleml4N  41425  dihmeetlem3N  41751  dihmeetlem13N  41765  mapdpglem32  42151  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  mzpcong  43400  iscnrm3rlem8  49422