Theorem con3rr3 156

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 153	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	com12 33	1 ⊢ (¬ 𝜒 → (𝜑 → ¬ 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  impi  165  dfbi1  216  ax13b  2065  mo2icl  3672  otsndisj  5492  uzwo  13031  ssnn0fi  14121  wrdnfi  14686  s3sndisj  15113  hmeofval  24070  alexsubALTlem4  24362  nbuhgr  29917  nb3grprlem2  29955  vtxdginducedm1lem4  30116  iswwlksnon  30435  clwwlkn  30610  clwwlknon  30674  cvnbtwn  32881  mh-regprimbi  37313  bj-fvimacnv0  38187  not12an2impnot1  45536