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 
|- -. ph
Assertion bianfi 
|- ( ph <-> ( ps /\ ph ) )

Proof

Step Hyp Ref Expression
1 bianfi.1 
 |-  -. ph
2 1 intnan 
 |-  -. ( ps /\ ph )
3 1 2 2false 
 |-  ( ph <-> ( ps /\ ph ) )