Theorem con3rr3 158

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 155	. 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  166  dfbi1  215  ax13b  2039  mo2icl  3707  otsndisj  5411  snnen2o  8709  uzwo  12314  ssnn0fi  13356  wrdnfi  13901  s3sndisj  14329  hmeofval  22368  alexsubALTlem4  22660  nbuhgr  27127  nb3grprlem2  27165  vtxdginducedm1lem4  27326  iswwlksnon  27633  clwwlkn  27806  clwwlknon  27871  cvnbtwn  30065  bj-fvimacnv0  34570  not12an2impnot1  40909