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  2031  mo2icl  3697  otsndisj  5494  snnen2oOLD  9234  uzwo  12925  ssnn0fi  14001  wrdnfi  14564  s3sndisj  14984  hmeofval  23694  alexsubALTlem4  23986  nbuhgr  29268  nb3grprlem2  29306  vtxdginducedm1lem4  29468  iswwlksnon  29781  clwwlkn  29953  clwwlknon  30017  cvnbtwn  32213  bj-fvimacnv0  37250  not12an2impnot1  44541