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  2035  mo2icl  3649  otsndisj  5433  snnen2oOLD  9010  uzwo  12651  ssnn0fi  13705  wrdnfi  14251  s3sndisj  14678  hmeofval  22909  alexsubALTlem4  23201  nbuhgr  27710  nb3grprlem2  27748  vtxdginducedm1lem4  27909  iswwlksnon  28218  clwwlkn  28390  clwwlknon  28454  cvnbtwn  30648  bj-fvimacnv0  35457  not12an2impnot1  42188