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  2036  mo2icl  3710  otsndisj  5519  snnen2oOLD  9224  uzwo  12892  ssnn0fi  13947  wrdnfi  14495  s3sndisj  14911  hmeofval  23254  alexsubALTlem4  23546  nbuhgr  28590  nb3grprlem2  28628  vtxdginducedm1lem4  28789  iswwlksnon  29097  clwwlkn  29269  clwwlknon  29333  cvnbtwn  31527  bj-fvimacnv0  36156  not12an2impnot1  43315