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  2067  mo2icl  3675  otsndisj  5499  uzwo  13078  ssnn0fi  14168  wrdnfi  14734  s3sndisj  15163  hmeofval  24132  alexsubALTlem4  24424  nbuhgr  29981  nb3grprlem2  30019  vtxdginducedm1lem4  30180  iswwlksnon  30499  clwwlkn  30674  clwwlknon  30738  cvnbtwn  32945  mh-regprimbi  37548  bj-fvimacnv0  38475  not12an2impnot1  45811