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  215  ax13b  2051  mo2icl  3675  otsndisj  5485  uzwo  12906  ssnn0fi  13992  wrdnfi  14555  s3sndisj  14974  hmeofval  23806  alexsubALTlem4  24098  nbuhgr  29501  nb3grprlem2  29539  vtxdginducedm1lem4  29700  iswwlksnon  30010  clwwlkn  30185  clwwlknon  30249  cvnbtwn  32446  mh-regprimbi  36866  bj-fvimacnv0  37739  not12an2impnot1  45105