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 
|- ( ph <-> -. ps )
Assertion con5i 
|- ( -. ph -> ps )

Proof

Step Hyp Ref Expression
1 con5i.1 
 |-  ( ph <-> -. ps )
2 con5 
 |-  ( ( ph <-> -. ps ) -> ( -. ph -> ps ) )
3 1 2 ax-mp 
 |-  ( -. ph -> ps )