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  1962  mo2icl  3379  sbcrextOLD  3506  otsndisj  4969  snnen2o  8134  uzwo  11736  ssnn0fi  12767  s3sndisj  13687  hmeofval  21542  alexsubALTlem4  21835  nbuhgr  26220  nbgrnself2  26240  nb3grprlem2  26264  vtxdginducedm1lem4  26419  cvnbtwn  29115  not12an2impnot1  38604