Theorem ifnefalse 4500

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 4497 directly in this case. It happens, e.g., in oevn0 8479. (Contributed by David A. Wheeler, 15-May-2015.)

Assertion

Ref	Expression
ifnefalse	⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)

Proof of Theorem ifnefalse

Step	Hyp	Ref	Expression
1		df-ne 2926	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		iffalse 4497	. 2 ⊢ (¬ 𝐴 = 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)
3	1, 2	sylbi 217	1 ⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-if 4489

This theorem is referenced by:  xpima2  6157  axcc2lem  10389  xnegmnf  13170  rexneg  13171  xaddpnf1  13186  xaddpnf2  13187  xaddmnf1  13188  xaddmnf2  13189  mnfaddpnf  13191  rexadd  13192  fztpval  13547  sadcp1  16425  smupp1  16450  pcval  16815  ramtcl  16981  ramub1lem1  16997  xpsfrnel  17525  gexlem2  19512  frgpuptinv  19701  frgpup3lem  19707  gsummpt1n0  19895  dprdfid  19949  dpjrid  19994  sdrgacs  20710  abvtrivd  20741  znf1o  21461  znhash  21468  znunithash  21474  mplsubrg  21914  psdmul  22053  mamulid  22328  mamurid  22329  dmatid  22382  dmatmulcl  22387  scmatdmat  22402  mdetdiagid  22487  chpdmatlem2  22726  chpscmat  22729  chpidmat  22734  xkoccn  23506  iccpnfhmeo  24843  xrhmeo  24844  ioorinv2  25476  mbfi1fseqlem4  25619  ellimc2  25778  dvcobr  25849  dvcobrOLD  25850  ply1remlem  26070  dvtaylp  26278  0cxp  26575  lgsval3  27226  lgsdinn0  27256  dchrisumlem1  27400  dchrvmasumiflem1  27412  rpvmasum2  27423  dchrvmasumlem  27434  padicabv  27541  indispconn  35221  ex-sategoelel  35408  fnejoin1  36356  ptrecube  37614  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  fdc  37739  cdlemk40f  40913  fiabv  42524  blenn0  48562