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  16183  axpasch  26727  3dimlem4  36615  3atlem4  36637  llncvrlpln2  36708  2lplnja  36770  lhpmcvr5N  37178  4atexlemswapqr  37214  4atexlemnclw  37221  trlval2  37314  cdleme21h  37485  cdleme24  37503  cdleme26ee  37511  cdleme26f  37514  cdleme26f2  37516  cdlemf1  37712  cdlemg16ALTN  37809  cdlemg17iqN  37825  cdlemg27b  37847  trlcone  37879  cdlemg48  37888  tendocan  37975  cdlemk26-3  38057  cdlemk27-3  38058  cdlemk28-3  38059  cdlemk37  38065  cdlemky  38077  cdlemk11ta  38080  cdlemkid3N  38084  cdlemk11t  38097  cdlemk46  38099  cdlemk47  38100  cdlemk51  38104  cdlemk52  38105  cdleml4N  38130  dihmeetlem1N  38441  dihmeetlem20N  38477  mapdpglem32  38856  addlimc  41949