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  16817  axpasch  28868  3dimlem4  39458  3atlem4  39480  llncvrlpln2  39551  2lplnja  39613  lhpmcvr5N  40021  4atexlemswapqr  40057  4atexlemnclw  40064  trlval2  40157  cdleme21h  40328  cdleme24  40346  cdleme26ee  40354  cdleme26f  40357  cdleme26f2  40359  cdlemf1  40555  cdlemg16ALTN  40652  cdlemg17iqN  40668  cdlemg27b  40690  trlcone  40722  cdlemg48  40731  tendocan  40818  cdlemk26-3  40900  cdlemk27-3  40901  cdlemk28-3  40902  cdlemk37  40908  cdlemky  40920  cdlemk11ta  40923  cdlemkid3N  40927  cdlemk11t  40940  cdlemk46  40942  cdlemk47  40943  cdlemk51  40947  cdlemk52  40948  cdleml4N  40973  dihmeetlem1N  41284  dihmeetlem20N  41320  mapdpglem32  41699  addlimc  45646  iscnrm3rlem8  48935