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  3679  otsndisj  5504  uzwo  12947  ssnn0fi  14035  wrdnfi  14599  s3sndisj  15024  hmeofval  23946  alexsubALTlem4  24238  nbuhgr  29727  nb3grprlem2  29765  vtxdginducedm1lem4  29926  iswwlksnon  30245  clwwlkn  30420  clwwlknon  30484  cvnbtwn  32685  mh-regprimbi  37089  bj-fvimacnv0  37963  not12an2impnot1  45310