Metamath Proof Explorer


Theorem con5i

Description: Inference form of con5 . (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis con5i.1 φ¬ψ
Assertion con5i ¬φψ

Proof

Step Hyp Ref Expression
1 con5i.1 φ¬ψ
2 con5 φ¬ψ¬φψ
3 1 2 ax-mp ¬φψ