Theorem con3rr3 158

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 155	. 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  166  dfbi1  215  ax13b  2035  mo2icl  3704  otsndisj  5401  snnen2o  8701  uzwo  12305  ssnn0fi  13347  wrdnfi  13893  s3sndisj  14321  hmeofval  22360  alexsubALTlem4  22652  nbuhgr  27119  nb3grprlem2  27157  vtxdginducedm1lem4  27318  iswwlksnon  27625  clwwlkn  27798  clwwlknon  27863  cvnbtwn  30057  bj-fvimacnv0  34562  not12an2impnot1  40895