Database
CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY
Propositional calculus
Logical negation
con3rr3
Next ⟩
nsyld
Metamath Proof Explorer
Ascii
Unicode
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
⊢
¬
χ
→
φ
→
¬
ψ