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  3672  otsndisj  5467  uzwo  12824  ssnn0fi  13908  wrdnfi  14471  s3sndisj  14890  hmeofval  23702  alexsubALTlem4  23994  nbuhgr  29416  nb3grprlem2  29454  vtxdginducedm1lem4  29616  iswwlksnon  29926  clwwlkn  30101  clwwlknon  30165  cvnbtwn  32361  bj-fvimacnv0  37491  not12an2impnot1  44809