Theorem simp12r 1288

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

Assertion

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

Proof of Theorem simp12r

Step	Hyp	Ref	Expression
1		simp2r 1201	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜓)
2	1	3ad2ant1 1133	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  10194  lsmcv  21058  nllyrest  23380  axcontlem4  28901  eqlkr  39099  athgt  39457  llncvrlpln2  39558  4atlem11b  39609  2lnat  39785  cdlemblem  39794  pclfinN  39901  lhp2at0nle  40036  4atexlemex6  40075  cdlemd2  40200  cdlemd8  40206  cdleme15a  40275  cdleme16b  40280  cdleme16c  40281  cdleme16d  40282  cdleme20h  40317  cdleme21c  40328  cdleme21ct  40330  cdleme22cN  40343  cdleme23b  40351  cdleme26fALTN  40363  cdleme26f  40364  cdleme26f2ALTN  40365  cdleme26f2  40366  cdleme32le  40448  cdleme35f  40455  cdlemf1  40562  trlord  40570  cdlemg7aN  40626  cdlemg33c0  40703  trlcone  40729  cdlemg44  40734  cdlemg48  40738  cdlemky  40927  cdlemk11ta  40930  cdleml4N  40980  dihmeetlem3N  41306  dihmeetlem13N  41320  mapdpglem32  41706  baerlem3lem2  41711  baerlem5alem2  41712  baerlem5blem2  41713  mzpcong  42968  iscnrm3rlem8  48939