Theorem simp13r 1306

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simp13r	⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓)

Proof of Theorem simp13r

Step	Hyp	Ref	Expression
1		simp3r 1219	. 2 ⊢ ((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2ant1 1149	1 ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  pceu  16894  axpasch  29196  3dimlem4  40095  3atlem4  40117  llncvrlpln2  40188  2lplnja  40250  lhpmcvr5N  40658  4atexlemswapqr  40694  4atexlemnclw  40701  trlval2  40794  cdleme21h  40965  cdleme24  40983  cdleme26ee  40991  cdleme26f  40994  cdleme26f2  40996  cdlemf1  41192  cdlemg16ALTN  41289  cdlemg17iqN  41305  cdlemg27b  41327  trlcone  41359  cdlemg48  41368  tendocan  41455  cdlemk26-3  41537  cdlemk27-3  41538  cdlemk28-3  41539  cdlemk37  41545  cdlemky  41557  cdlemk11ta  41560  cdlemkid3N  41564  cdlemk11t  41577  cdlemk46  41579  cdlemk47  41580  cdlemk51  41584  cdlemk52  41585  cdleml4N  41610  dihmeetlem1N  41921  dihmeetlem20N  41957  mapdpglem32  42336  addlimc  46221  iscnrm3rlem8  49577