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  16944  axpasch  29406  3dimlem4  40345  3atlem4  40367  llncvrlpln2  40438  2lplnja  40500  lhpmcvr5N  40908  4atexlemswapqr  40944  4atexlemnclw  40951  trlval2  41044  cdleme21h  41215  cdleme24  41233  cdleme26ee  41241  cdleme26f  41244  cdleme26f2  41246  cdlemf1  41442  cdlemg16ALTN  41539  cdlemg17iqN  41555  cdlemg27b  41577  trlcone  41609  cdlemg48  41618  tendocan  41705  cdlemk26-3  41787  cdlemk27-3  41788  cdlemk28-3  41789  cdlemk37  41795  cdlemky  41807  cdlemk11ta  41810  cdlemkid3N  41814  cdlemk11t  41827  cdlemk46  41829  cdlemk47  41830  cdlemk51  41834  cdlemk52  41835  cdleml4N  41860  dihmeetlem1N  42171  dihmeetlem20N  42207  mapdpglem32  42586  addlimc  46484  iscnrm3rlem8  49881