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  3660  otsndisj  5473  uzwo  12861  ssnn0fi  13947  wrdnfi  14510  s3sndisj  14929  hmeofval  23723  alexsubALTlem4  24015  nbuhgr  29412  nb3grprlem2  29450  vtxdginducedm1lem4  29611  iswwlksnon  29921  clwwlkn  30096  clwwlknon  30160  cvnbtwn  32357  mh-regprimbi  36727  bj-fvimacnv0  37600  not12an2impnot1  44995