Theorem simp13r 1177

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

Assertion

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

Proof of Theorem simp13r

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  pceu  15551  axpasch  25821  3dimlem4  34750  3atlem4  34772  llncvrlpln2  34843  2lplnja  34905  lhpmcvr5N  35313  4atexlemswapqr  35349  4atexlemnclw  35356  trlval2  35450  cdleme21h  35622  cdleme24  35640  cdleme26ee  35648  cdleme26f  35651  cdleme26f2  35653  cdlemf1  35849  cdlemg16ALTN  35946  cdlemg17iqN  35962  cdlemg27b  35984  trlcone  36016  cdlemg48  36025  tendocan  36112  cdlemk26-3  36194  cdlemk27-3  36195  cdlemk28-3  36196  cdlemk37  36202  cdlemky  36214  cdlemk11ta  36217  cdlemkid3N  36221  cdlemk11t  36234  cdlemk46  36236  cdlemk47  36237  cdlemk51  36241  cdlemk52  36242  cdleml4N  36267  dihmeetlem1N  36579  dihmeetlem20N  36615  mapdpglem32  36994  addlimc  39880