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  213  ax13b  2033  mo2icl  3668  otsndisj  5454  uzwo  12804  ssnn0fi  13887  wrdnfi  14450  s3sndisj  14869  hmeofval  23668  alexsubALTlem4  23960  nbuhgr  29316  nb3grprlem2  29354  vtxdginducedm1lem4  29516  iswwlksnon  29826  clwwlkn  29998  clwwlknon  30062  cvnbtwn  32258  bj-fvimacnv0  37320  not12an2impnot1  44601