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  10147  lsmcv  21066  nllyrest  23389  axcontlem4  28930  eqlkr  39077  athgt  39435  llncvrlpln2  39536  4atlem11b  39587  2lnat  39763  cdlemblem  39772  pclfinN  39879  lhp2at0nle  40014  4atexlemex6  40053  cdlemd2  40178  cdlemd8  40184  cdleme15a  40253  cdleme16b  40258  cdleme16c  40259  cdleme16d  40260  cdleme20h  40295  cdleme21c  40306  cdleme21ct  40308  cdleme22cN  40321  cdleme23b  40329  cdleme26fALTN  40341  cdleme26f  40342  cdleme26f2ALTN  40343  cdleme26f2  40344  cdleme32le  40426  cdleme35f  40433  cdlemf1  40540  trlord  40548  cdlemg7aN  40604  cdlemg33c0  40681  trlcone  40707  cdlemg44  40712  cdlemg48  40716  cdlemky  40905  cdlemk11ta  40908  cdleml4N  40958  dihmeetlem3N  41284  dihmeetlem13N  41298  mapdpglem32  41684  baerlem3lem2  41689  baerlem5alem2  41690  baerlem5blem2  41691  mzpcong  42945  iscnrm3rlem8  48932