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 1133	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  16762  axpasch  28923  3dimlem4  39586  3atlem4  39608  llncvrlpln2  39679  2lplnja  39741  lhpmcvr5N  40149  4atexlemswapqr  40185  4atexlemnclw  40192  trlval2  40285  cdleme21h  40456  cdleme24  40474  cdleme26ee  40482  cdleme26f  40485  cdleme26f2  40487  cdlemf1  40683  cdlemg16ALTN  40780  cdlemg17iqN  40796  cdlemg27b  40818  trlcone  40850  cdlemg48  40859  tendocan  40946  cdlemk26-3  41028  cdlemk27-3  41029  cdlemk28-3  41030  cdlemk37  41036  cdlemky  41048  cdlemk11ta  41051  cdlemkid3N  41055  cdlemk11t  41068  cdlemk46  41070  cdlemk47  41071  cdlemk51  41075  cdlemk52  41076  cdleml4N  41101  dihmeetlem1N  41412  dihmeetlem20N  41448  mapdpglem32  41827  addlimc  45773  iscnrm3rlem8  49074