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  212  ax13b  2033  mo2icl  3709  otsndisj  5518  snnen2oOLD  9229  uzwo  12899  ssnn0fi  13954  wrdnfi  14502  s3sndisj  14918  hmeofval  23482  alexsubALTlem4  23774  nbuhgr  28867  nb3grprlem2  28905  vtxdginducedm1lem4  29066  iswwlksnon  29374  clwwlkn  29546  clwwlknon  29610  cvnbtwn  31806  bj-fvimacnv0  36470  not12an2impnot1  43631