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  2030  mo2icl  3719  otsndisj  5523  snnen2oOLD  9265  uzwo  12954  ssnn0fi  14027  wrdnfi  14587  s3sndisj  15007  hmeofval  23767  alexsubALTlem4  24059  nbuhgr  29361  nb3grprlem2  29399  vtxdginducedm1lem4  29561  iswwlksnon  29874  clwwlkn  30046  clwwlknon  30110  cvnbtwn  32306  bj-fvimacnv0  37288  not12an2impnot1  44593