Theorem con3rr3 156

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 153	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	com12 33	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  165  dfbi1  216  ax13b  2059  mo2icl  3686  otsndisj  5500  uzwo  12931  ssnn0fi  14017  wrdnfi  14581  s3sndisj  15000  hmeofval  23880  alexsubALTlem4  24172  nbuhgr  29630  nb3grprlem2  29668  vtxdginducedm1lem4  29829  iswwlksnon  30139  clwwlkn  30314  clwwlknon  30378  cvnbtwn  32575  mh-regprimbi  36941  bj-fvimacnv0  37813  not12an2impnot1  45162