Metamath Proof Explorer


Theorem con3rr3

Description: Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013)

Ref Expression
Hypothesis con3rr3.1 ⊢ φ → ψ → χ
Assertion con3rr3 ⊢ ¬ χ → φ → ¬ ψ

Proof

Step Hyp Ref Expression
1 con3rr3.1 ⊢ φ → ψ → χ
2 1 con3d ⊢ φ → ¬ χ → ¬ ψ
3 2 com12 ⊢ ¬ χ → φ → ¬ ψ