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  2029  mo2icl  3723  otsndisj  5529  snnen2oOLD  9262  uzwo  12951  ssnn0fi  14023  wrdnfi  14583  s3sndisj  15003  hmeofval  23782  alexsubALTlem4  24074  nbuhgr  29375  nb3grprlem2  29413  vtxdginducedm1lem4  29575  iswwlksnon  29883  clwwlkn  30055  clwwlknon  30119  cvnbtwn  32315  bj-fvimacnv0  37269  not12an2impnot1  44566