Theorem simp13r 1288

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

Assertion

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

Proof of Theorem simp13r

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  pceu  16547  axpasch  27309  3dimlem4  37478  3atlem4  37500  llncvrlpln2  37571  2lplnja  37633  lhpmcvr5N  38041  4atexlemswapqr  38077  4atexlemnclw  38084  trlval2  38177  cdleme21h  38348  cdleme24  38366  cdleme26ee  38374  cdleme26f  38377  cdleme26f2  38379  cdlemf1  38575  cdlemg16ALTN  38672  cdlemg17iqN  38688  cdlemg27b  38710  trlcone  38742  cdlemg48  38751  tendocan  38838  cdlemk26-3  38920  cdlemk27-3  38921  cdlemk28-3  38922  cdlemk37  38928  cdlemky  38940  cdlemk11ta  38943  cdlemkid3N  38947  cdlemk11t  38960  cdlemk46  38962  cdlemk47  38963  cdlemk51  38967  cdlemk52  38968  cdleml4N  38993  dihmeetlem1N  39304  dihmeetlem20N  39340  mapdpglem32  39719  addlimc  43189  iscnrm3rlem8  46241