Theorem simp13r 1308

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

Assertion

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

Proof of Theorem simp13r

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  pceu  16907  axpasch  29272  3dimlem4  40219  3atlem4  40241  llncvrlpln2  40312  2lplnja  40374  lhpmcvr5N  40782  4atexlemswapqr  40818  4atexlemnclw  40825  trlval2  40918  cdleme21h  41089  cdleme24  41107  cdleme26ee  41115  cdleme26f  41118  cdleme26f2  41120  cdlemf1  41316  cdlemg16ALTN  41413  cdlemg17iqN  41429  cdlemg27b  41451  trlcone  41483  cdlemg48  41492  tendocan  41579  cdlemk26-3  41661  cdlemk27-3  41662  cdlemk28-3  41663  cdlemk37  41669  cdlemky  41681  cdlemk11ta  41684  cdlemkid3N  41688  cdlemk11t  41701  cdlemk46  41703  cdlemk47  41704  cdlemk51  41708  cdlemk52  41709  cdleml4N  41734  dihmeetlem1N  42045  dihmeetlem20N  42081  mapdpglem32  42460  addlimc  46345  iscnrm3rlem8  49708