Metamath Proof Explorer


Theorem elif

Description: Membership in a conditional operator. (Contributed by NM, 14-Feb-2005)

Ref Expression
Assertion elif A if φ B C φ A B ¬ φ A C

Proof

Step Hyp Ref Expression
1 eleq2 if φ B C = B A if φ B C A B
2 eleq2 if φ B C = C A if φ B C A C
3 1 2 elimif A if φ B C φ A B ¬ φ A C