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  2062  mo2icl  3678  otsndisj  5504  uzwo  12936  ssnn0fi  14023  wrdnfi  14587  s3sndisj  15006  hmeofval  23896  alexsubALTlem4  24188  nbuhgr  29674  nb3grprlem2  29712  vtxdginducedm1lem4  29873  iswwlksnon  30183  clwwlkn  30358  clwwlknon  30422  cvnbtwn  32619  mh-regprimbi  37037  bj-fvimacnv0  37911  not12an2impnot1  45260