Metamath Proof Explorer

Theorem bj-ntrufal

Description: The negation of a theorem is equivalent to false. This can shorten dfnul2 . (Contributed by BJ, 5-Oct-2024)

Ref Expression
Hypothesis bj-ntrufal.1 
|- ph
Assertion bj-ntrufal 
|- ( -. ph <-> F. )

Proof

Step Hyp Ref Expression
1 bj-ntrufal.1 
 |-  ph
2 1 notnoti 
 |-  -. -. ph
3 2 bifal 
 |-  ( -. ph <-> F. )