Metamath Proof Explorer


Theorem bianfi

Description: A wff conjoined with falsehood is false. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 26-Nov-2012)

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

Proof

Step Hyp Ref Expression
1 bianfi.1 ¬φ
2 1 intnan ¬ψφ
3 1 2 2false φψφ