Metamath Proof Explorer

Theorem bifald

Description: Infer the equivalence to a contradiction from a negation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017)

Ref Expression
Hypothesis bifald.1 
|- ( ph -> -. ps )
Assertion bifald 
|- ( ph -> ( ps <-> F. ) )

Proof

Step Hyp Ref Expression
1 bifald.1 
 |-  ( ph -> -. ps )
2 id 
 |-  ( ps -> ps )
3 falim 
 |-  ( F. -> ps )
4 2 3 pm5.21ni 
 |-  ( -. ps -> ( ps <-> F. ) )
5 1 4 syl 
 |-  ( ph -> ( ps <-> F. ) )