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  2033  mo2icl  3669  otsndisj  5464  uzwo  12815  ssnn0fi  13899  wrdnfi  14462  s3sndisj  14881  hmeofval  23693  alexsubALTlem4  23985  nbuhgr  29342  nb3grprlem2  29380  vtxdginducedm1lem4  29542  iswwlksnon  29852  clwwlkn  30027  clwwlknon  30091  cvnbtwn  32287  bj-fvimacnv0  37403  not12an2impnot1  44725