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  16750  axpasch  28912  3dimlem4  39482  3atlem4  39504  llncvrlpln2  39575  2lplnja  39637  lhpmcvr5N  40045  4atexlemswapqr  40081  4atexlemnclw  40088  trlval2  40181  cdleme21h  40352  cdleme24  40370  cdleme26ee  40378  cdleme26f  40381  cdleme26f2  40383  cdlemf1  40579  cdlemg16ALTN  40676  cdlemg17iqN  40692  cdlemg27b  40714  trlcone  40746  cdlemg48  40755  tendocan  40842  cdlemk26-3  40924  cdlemk27-3  40925  cdlemk28-3  40926  cdlemk37  40932  cdlemky  40944  cdlemk11ta  40947  cdlemkid3N  40951  cdlemk11t  40964  cdlemk46  40966  cdlemk47  40967  cdlemk51  40971  cdlemk52  40972  cdleml4N  40997  dihmeetlem1N  41308  dihmeetlem20N  41344  mapdpglem32  41723  addlimc  45665  iscnrm3rlem8  48957