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  2032  mo2icl  3685  otsndisj  5479  uzwo  12870  ssnn0fi  13950  wrdnfi  14513  s3sndisj  14933  hmeofval  23645  alexsubALTlem4  23937  nbuhgr  29270  nb3grprlem2  29308  vtxdginducedm1lem4  29470  iswwlksnon  29783  clwwlkn  29955  clwwlknon  30019  cvnbtwn  32215  bj-fvimacnv0  37274  not12an2impnot1  44558