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  5496  uzwo  12960  ssnn0fi  14049  wrdnfi  14613  s3sndisj  15040  hmeofval  23984  alexsubALTlem4  24276  nbuhgr  29803  nb3grprlem2  29841  vtxdginducedm1lem4  30002  iswwlksnon  30321  clwwlkn  30496  clwwlknon  30560  cvnbtwn  32767  mh-regprimbi  37164  bj-fvimacnv0  38038  not12an2impnot1  45391