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  17029  axpasch  29524  3dimlem4  40614  3atlem4  40636  llncvrlpln2  40707  2lplnja  40769  lhpmcvr5N  41177  4atexlemswapqr  41213  4atexlemnclw  41220  trlval2  41313  cdleme21h  41484  cdleme24  41502  cdleme26ee  41510  cdleme26f  41513  cdleme26f2  41515  cdlemf1  41711  cdlemg16ALTN  41808  cdlemg17iqN  41824  cdlemg27b  41846  trlcone  41878  cdlemg48  41887  tendocan  41974  cdlemk26-3  42056  cdlemk27-3  42057  cdlemk28-3  42058  cdlemk37  42064  cdlemky  42076  cdlemk11ta  42079  cdlemkid3N  42083  cdlemk11t  42096  cdlemk46  42098  cdlemk47  42099  cdlemk51  42103  cdlemk52  42104  cdleml4N  42129  dihmeetlem1N  42440  dihmeetlem20N  42476  mapdpglem32  42855  addlimc  46751  iscnrm3rlem8  50154