Theorem simp13r 1290

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

Assertion

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

Proof of Theorem simp13r

Step	Hyp	Ref	Expression
1		simp3r 1203	. 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:  pceu  16866  axpasch  28920  3dimlem4  39483  3atlem4  39505  llncvrlpln2  39576  2lplnja  39638  lhpmcvr5N  40046  4atexlemswapqr  40082  4atexlemnclw  40089  trlval2  40182  cdleme21h  40353  cdleme24  40371  cdleme26ee  40379  cdleme26f  40382  cdleme26f2  40384  cdlemf1  40580  cdlemg16ALTN  40677  cdlemg17iqN  40693  cdlemg27b  40715  trlcone  40747  cdlemg48  40756  tendocan  40843  cdlemk26-3  40925  cdlemk27-3  40926  cdlemk28-3  40927  cdlemk37  40933  cdlemky  40945  cdlemk11ta  40948  cdlemkid3N  40952  cdlemk11t  40965  cdlemk46  40967  cdlemk47  40968  cdlemk51  40972  cdlemk52  40973  cdleml4N  40998  dihmeetlem1N  41309  dihmeetlem20N  41345  mapdpglem32  41724  addlimc  45677  iscnrm3rlem8  48921