Theorem con3rr3 155

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 152	. 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  164  dfbi1  214  ax13b  2039  mo2icl  3662  otsndisj  5467  uzwo  12859  ssnn0fi  13945  wrdnfi  14508  s3sndisj  14927  hmeofval  23748  alexsubALTlem4  24040  nbuhgr  29437  nb3grprlem2  29475  vtxdginducedm1lem4  29636  iswwlksnon  29946  clwwlkn  30121  clwwlknon  30185  cvnbtwn  32382  mh-regprimbi  36780  bj-fvimacnv0  37653  not12an2impnot1  45019