Theorem con3rr3 151

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 148	. 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  160  ax13b  1964  mo2icl  3385  sbcrextOLD  3512  otsndisj  4979  snnen2o  8149  uzwo  11751  ssnn0fi  12784  s3sndisj  13706  hmeofval  21561  alexsubALTlem4  21854  nbuhgr  26239  nbgrnself2  26259  nb3grprlem2  26283  vtxdginducedm1lem4  26438  cvnbtwn  29145  not12an2impnot1  38784