Theorem con3rr3 155

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

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  impi  164  dfbi1  213  ax13b  2032  mo2icl  3702  otsndisj  5499  snnen2oOLD  9241  uzwo  12932  ssnn0fi  14008  wrdnfi  14571  s3sndisj  14991  hmeofval  23701  alexsubALTlem4  23993  nbuhgr  29327  nb3grprlem2  29365  vtxdginducedm1lem4  29527  iswwlksnon  29840  clwwlkn  30012  clwwlknon  30076  cvnbtwn  32272  bj-fvimacnv0  37309  not12an2impnot1  44560