Theorem simp13r 1285

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

Assertion

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

Proof of Theorem simp13r

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  pceu  16177  axpasch  26721  3dimlem4  36594  3atlem4  36616  llncvrlpln2  36687  2lplnja  36749  lhpmcvr5N  37157  4atexlemswapqr  37193  4atexlemnclw  37200  trlval2  37293  cdleme21h  37464  cdleme24  37482  cdleme26ee  37490  cdleme26f  37493  cdleme26f2  37495  cdlemf1  37691  cdlemg16ALTN  37788  cdlemg17iqN  37804  cdlemg27b  37826  trlcone  37858  cdlemg48  37867  tendocan  37954  cdlemk26-3  38036  cdlemk27-3  38037  cdlemk28-3  38038  cdlemk37  38044  cdlemky  38056  cdlemk11ta  38059  cdlemkid3N  38063  cdlemk11t  38076  cdlemk46  38078  cdlemk47  38079  cdlemk51  38083  cdlemk52  38084  cdleml4N  38109  dihmeetlem1N  38420  dihmeetlem20N  38456  mapdpglem32  38835  addlimc  41922