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  3711  otsndisj  5520  snnen2oOLD  9227  uzwo  12895  ssnn0fi  13950  wrdnfi  14498  s3sndisj  14914  hmeofval  23262  alexsubALTlem4  23554  nbuhgr  28600  nb3grprlem2  28638  vtxdginducedm1lem4  28799  iswwlksnon  29107  clwwlkn  29279  clwwlknon  29343  cvnbtwn  31539  bj-fvimacnv0  36167  not12an2impnot1  43329