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 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  16879  axpasch  28970  3dimlem4  39446  3atlem4  39468  llncvrlpln2  39539  2lplnja  39601  lhpmcvr5N  40009  4atexlemswapqr  40045  4atexlemnclw  40052  trlval2  40145  cdleme21h  40316  cdleme24  40334  cdleme26ee  40342  cdleme26f  40345  cdleme26f2  40347  cdlemf1  40543  cdlemg16ALTN  40640  cdlemg17iqN  40656  cdlemg27b  40678  trlcone  40710  cdlemg48  40719  tendocan  40806  cdlemk26-3  40888  cdlemk27-3  40889  cdlemk28-3  40890  cdlemk37  40896  cdlemky  40908  cdlemk11ta  40911  cdlemkid3N  40915  cdlemk11t  40928  cdlemk46  40930  cdlemk47  40931  cdlemk51  40935  cdlemk52  40936  cdleml4N  40961  dihmeetlem1N  41272  dihmeetlem20N  41308  mapdpglem32  41687  addlimc  45603  iscnrm3rlem8  48743