Theorem simp13r 1286

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

Assertion

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

Proof of Theorem simp13r

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  pceu  16173  axpasch  26735  3dimlem4  36760  3atlem4  36782  llncvrlpln2  36853  2lplnja  36915  lhpmcvr5N  37323  4atexlemswapqr  37359  4atexlemnclw  37366  trlval2  37459  cdleme21h  37630  cdleme24  37648  cdleme26ee  37656  cdleme26f  37659  cdleme26f2  37661  cdlemf1  37857  cdlemg16ALTN  37954  cdlemg17iqN  37970  cdlemg27b  37992  trlcone  38024  cdlemg48  38033  tendocan  38120  cdlemk26-3  38202  cdlemk27-3  38203  cdlemk28-3  38204  cdlemk37  38210  cdlemky  38222  cdlemk11ta  38225  cdlemkid3N  38229  cdlemk11t  38242  cdlemk46  38244  cdlemk47  38245  cdlemk51  38249  cdlemk52  38250  cdleml4N  38275  dihmeetlem1N  38586  dihmeetlem20N  38622  mapdpglem32  39001  addlimc  42290