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  2035  mo2icl  3650  otsndisj  5435  snnen2oOLD  9008  uzwo  12649  ssnn0fi  13703  wrdnfi  14249  s3sndisj  14676  hmeofval  22907  alexsubALTlem4  23199  nbuhgr  27708  nb3grprlem2  27746  vtxdginducedm1lem4  27907  iswwlksnon  28215  clwwlkn  28387  clwwlknon  28451  cvnbtwn  30645  bj-fvimacnv0  35454  not12an2impnot1  42158