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  212  ax13b  2027  mo2icl  3706  otsndisj  5521  snnen2oOLD  9255  uzwo  12933  ssnn0fi  13991  wrdnfi  14542  s3sndisj  14958  hmeofval  23723  alexsubALTlem4  24015  nbuhgr  29248  nb3grprlem2  29286  vtxdginducedm1lem4  29448  iswwlksnon  29756  clwwlkn  29928  clwwlknon  29992  cvnbtwn  32188  bj-fvimacnv0  36916  not12an2impnot1  44154