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  2034  mo2icl  3674  otsndisj  5475  uzwo  12836  ssnn0fi  13920  wrdnfi  14483  s3sndisj  14902  hmeofval  23714  alexsubALTlem4  24006  nbuhgr  29428  nb3grprlem2  29466  vtxdginducedm1lem4  29628  iswwlksnon  29938  clwwlkn  30113  clwwlknon  30177  cvnbtwn  32373  bj-fvimacnv0  37538  not12an2impnot1  44921