Metamath Proof Explorer


Theorem iffalsei

Description: Inference associated with iffalse . (Contributed by BJ, 7-Oct-2018)

Ref Expression
Hypothesis iffalsei.1 ¬φ
Assertion iffalsei ifφAB=B

Proof

Step Hyp Ref Expression
1 iffalsei.1 ¬φ
2 iffalse ¬φifφAB=B
3 1 2 ax-mp ifφAB=B