Theorem con3rr3 158

Description: Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.)

Hypothesis

Ref	Expression
con3rr3.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
con3rr3	⊢ (¬ 𝜒 → (𝜑 → ¬ 𝜓))

Proof of Theorem con3rr3

Step	Hyp	Ref	Expression
1		con3rr3.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	con3d 155	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	com12 32	1 ⊢ (¬ 𝜒 → (𝜑 → ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  impi  167  dfbi1  216  ax13b  2039  mo2icl  3653  otsndisj  5374  snnen2o  8691  uzwo  12299  ssnn0fi  13348  wrdnfi  13891  s3sndisj  14318  hmeofval  22363  alexsubALTlem4  22655  nbuhgr  27133  nb3grprlem2  27171  vtxdginducedm1lem4  27332  iswwlksnon  27639  clwwlkn  27811  clwwlknon  27875  cvnbtwn  30069  bj-fvimacnv0  34701  not12an2impnot1  41274