Metamath Proof Explorer


Theorem elif

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

Ref Expression
Assertion elif AifφBCφAB¬φAC

Proof

Step Hyp Ref Expression
1 eleq2 ifφBC=BAifφBCAB
2 eleq2 ifφBC=CAifφBCAC
3 1 2 elimif AifφBCφAB¬φAC