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  2032  mo2icl  3688  otsndisj  5482  uzwo  12877  ssnn0fi  13957  wrdnfi  14520  s3sndisj  14940  hmeofval  23652  alexsubALTlem4  23944  nbuhgr  29277  nb3grprlem2  29315  vtxdginducedm1lem4  29477  iswwlksnon  29790  clwwlkn  29962  clwwlknon  30026  cvnbtwn  32222  bj-fvimacnv0  37281  not12an2impnot1  44565