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  16774  axpasch  29014  3dimlem4  39724  3atlem4  39746  llncvrlpln2  39817  2lplnja  39879  lhpmcvr5N  40287  4atexlemswapqr  40323  4atexlemnclw  40330  trlval2  40423  cdleme21h  40594  cdleme24  40612  cdleme26ee  40620  cdleme26f  40623  cdleme26f2  40625  cdlemf1  40821  cdlemg16ALTN  40918  cdlemg17iqN  40934  cdlemg27b  40956  trlcone  40988  cdlemg48  40997  tendocan  41084  cdlemk26-3  41166  cdlemk27-3  41167  cdlemk28-3  41168  cdlemk37  41174  cdlemky  41186  cdlemk11ta  41189  cdlemkid3N  41193  cdlemk11t  41206  cdlemk46  41208  cdlemk47  41209  cdlemk51  41213  cdlemk52  41214  cdleml4N  41239  dihmeetlem1N  41550  dihmeetlem20N  41586  mapdpglem32  41965  addlimc  45892  iscnrm3rlem8  49192