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 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pceu  17004  axpasch  29501  3dimlem4  40489  3atlem4  40511  llncvrlpln2  40582  2lplnja  40644  lhpmcvr5N  41052  4atexlemswapqr  41088  4atexlemnclw  41095  trlval2  41188  cdleme21h  41359  cdleme24  41377  cdleme26ee  41385  cdleme26f  41388  cdleme26f2  41390  cdlemf1  41586  cdlemg16ALTN  41683  cdlemg17iqN  41699  cdlemg27b  41721  trlcone  41753  cdlemg48  41762  tendocan  41849  cdlemk26-3  41931  cdlemk27-3  41932  cdlemk28-3  41933  cdlemk37  41939  cdlemky  41951  cdlemk11ta  41954  cdlemkid3N  41958  cdlemk11t  41971  cdlemk46  41973  cdlemk47  41974  cdlemk51  41978  cdlemk52  41979  cdleml4N  42004  dihmeetlem1N  42315  dihmeetlem20N  42351  mapdpglem32  42730  addlimc  46602  iscnrm3rlem8  49999