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 1134	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  pceu  16779  axpasch  28230  3dimlem4  38383  3atlem4  38405  llncvrlpln2  38476  2lplnja  38538  lhpmcvr5N  38946  4atexlemswapqr  38982  4atexlemnclw  38989  trlval2  39082  cdleme21h  39253  cdleme24  39271  cdleme26ee  39279  cdleme26f  39282  cdleme26f2  39284  cdlemf1  39480  cdlemg16ALTN  39577  cdlemg17iqN  39593  cdlemg27b  39615  trlcone  39647  cdlemg48  39656  tendocan  39743  cdlemk26-3  39825  cdlemk27-3  39826  cdlemk28-3  39827  cdlemk37  39833  cdlemky  39845  cdlemk11ta  39848  cdlemkid3N  39852  cdlemk11t  39865  cdlemk46  39867  cdlemk47  39868  cdlemk51  39872  cdlemk52  39873  cdleml4N  39898  dihmeetlem1N  40209  dihmeetlem20N  40245  mapdpglem32  40624  addlimc  44412  iscnrm3rlem8  47628