Theorem ifnefalse 3620

Description: When values are unequal, but an "if" condition checks if they are equal, then the "false" branch results. This is a simple utility to provide a slight shortening and simplification of proofs versus applying iffalse 3617 directly in this case. (Contributed by David A. Wheeler, 15-May-2015.)

Assertion

Ref	Expression
ifnefalse	|- ( A =/= B -> if ( A = B , C , D ) = D )

Proof of Theorem ifnefalse

Step	Hyp	Ref	Expression
1		df-ne 2404	. 2 |- ( A =/= B <-> -. A = B )
2		iffalse 3617	. 2 |- ( -. A = B -> if ( A = B , C , D ) = D )
3	1, 2	sylbi 121	1 |- ( A =/= B -> if ( A = B , C , D ) = D )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1398   =/= wne 2403   ifcif 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-ne 2404  df-if 3608

This theorem is referenced by:  xnegmnf  10108  rexneg  10109  xaddpnf1  10125  xaddpnf2  10126  xaddmnf1  10127  xaddmnf2  10128  mnfaddpnf  10130  rexadd  10131  fztpval  10363  pcval  12932  xpsfrnel  13490  znf1o  14730  znfi  14734  znhash  14735  lgsval3  15820  lgsdinn0  15850