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  2036  mo2icl  3644  otsndisj  5427  snnen2o  8903  uzwo  12580  ssnn0fi  13633  wrdnfi  14179  s3sndisj  14606  hmeofval  22817  alexsubALTlem4  23109  nbuhgr  27613  nb3grprlem2  27651  vtxdginducedm1lem4  27812  iswwlksnon  28119  clwwlkn  28291  clwwlknon  28355  cvnbtwn  30549  bj-fvimacnv0  35384  not12an2impnot1  42077