Metamath Proof Explorer

Theorem bianfd

Description: A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995) (Proof shortened by Wolf Lammen, 5-Nov-2013)

Ref Expression
Hypothesis bianfd.1 
|- ( ph -> -. ps )
Assertion bianfd 
|- ( ph -> ( ps <-> ( ps /\ ch ) ) )

Proof

Step Hyp Ref Expression
1 bianfd.1 
 |-  ( ph -> -. ps )
2 1 intnanrd 
 |-  ( ph -> -. ( ps /\ ch ) )
3 1 2 2falsed 
 |-  ( ph -> ( ps <-> ( ps /\ ch ) ) )