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  3736  otsndisj  5538  snnen2oOLD  9290  uzwo  12976  ssnn0fi  14036  wrdnfi  14596  s3sndisj  15016  hmeofval  23787  alexsubALTlem4  24079  nbuhgr  29378  nb3grprlem2  29416  vtxdginducedm1lem4  29578  iswwlksnon  29886  clwwlkn  30058  clwwlknon  30122  cvnbtwn  32318  bj-fvimacnv0  37252  not12an2impnot1  44539