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  2064  mo2icl  3671  otsndisj  5491  uzwo  13043  ssnn0fi  14133  wrdnfi  14698  s3sndisj  15127  hmeofval  24084  alexsubALTlem4  24376  nbuhgr  29931  nb3grprlem2  29969  vtxdginducedm1lem4  30130  iswwlksnon  30449  clwwlkn  30624  clwwlknon  30688  cvnbtwn  32895  mh-regprimbi  37427  bj-fvimacnv0  38314  not12an2impnot1  45658