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 ¬ χ φ ¬ ψ