Theorem simp12r 1286

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

Assertion

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

Proof of Theorem simp12r

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

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

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 1088

This theorem is referenced by:  ackbij1lem16  10272  lsmcv  21161  nllyrest  23510  axcontlem4  28997  eqlkr  39081  athgt  39439  llncvrlpln2  39540  4atlem11b  39591  2lnat  39767  cdlemblem  39776  pclfinN  39883  lhp2at0nle  40018  4atexlemex6  40057  cdlemd2  40182  cdlemd8  40188  cdleme15a  40257  cdleme16b  40262  cdleme16c  40263  cdleme16d  40264  cdleme20h  40299  cdleme21c  40310  cdleme21ct  40312  cdleme22cN  40325  cdleme23b  40333  cdleme26fALTN  40345  cdleme26f  40346  cdleme26f2ALTN  40347  cdleme26f2  40348  cdleme32le  40430  cdleme35f  40437  cdlemf1  40544  trlord  40552  cdlemg7aN  40608  cdlemg33c0  40685  trlcone  40711  cdlemg44  40716  cdlemg48  40720  cdlemky  40909  cdlemk11ta  40912  cdleml4N  40962  dihmeetlem3N  41288  dihmeetlem13N  41302  mapdpglem32  41688  baerlem3lem2  41693  baerlem5alem2  41694  baerlem5blem2  41695  mzpcong  42961  iscnrm3rlem8  48744