Metamath Proof Explorer


Theorem iffalsed

Description: Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis iffalsed.1 φ ¬ χ
Assertion iffalsed φ if χ A B = B

Proof

Step Hyp Ref Expression
1 iffalsed.1 φ ¬ χ
2 iffalse ¬ χ if χ A B = B
3 1 2 syl φ if χ A B = B