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  3661  otsndisj  5467  uzwo  12852  ssnn0fi  13938  wrdnfi  14501  s3sndisj  14920  hmeofval  23733  alexsubALTlem4  24025  nbuhgr  29426  nb3grprlem2  29464  vtxdginducedm1lem4  29626  iswwlksnon  29936  clwwlkn  30111  clwwlknon  30175  cvnbtwn  32372  mh-regprimbi  36743  bj-fvimacnv0  37616  not12an2impnot1  45013