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  3676  otsndisj  5466  uzwo  12830  ssnn0fi  13910  wrdnfi  14473  s3sndisj  14892  hmeofval  23661  alexsubALTlem4  23953  nbuhgr  29306  nb3grprlem2  29344  vtxdginducedm1lem4  29506  iswwlksnon  29816  clwwlkn  29988  clwwlknon  30052  cvnbtwn  32248  bj-fvimacnv0  37262  not12an2impnot1  44545