Theorem ifnefalse 4503

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2926  ifcif 4491

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-if 4492

This theorem is referenced by:  xpima2  6160  axcc2lem  10396  xnegmnf  13177  rexneg  13178  xaddpnf1  13193  xaddpnf2  13194  xaddmnf1  13195  xaddmnf2  13196  mnfaddpnf  13198  rexadd  13199  fztpval  13554  sadcp1  16432  smupp1  16457  pcval  16822  ramtcl  16988  ramub1lem1  17004  xpsfrnel  17532  gexlem2  19519  frgpuptinv  19708  frgpup3lem  19714  gsummpt1n0  19902  dprdfid  19956  dpjrid  20001  sdrgacs  20717  abvtrivd  20748  znf1o  21468  znhash  21475  znunithash  21481  mplsubrg  21921  psdmul  22060  mamulid  22335  mamurid  22336  dmatid  22389  dmatmulcl  22394  scmatdmat  22409  mdetdiagid  22494  chpdmatlem2  22733  chpscmat  22736  chpidmat  22741  xkoccn  23513  iccpnfhmeo  24850  xrhmeo  24851  ioorinv2  25483  mbfi1fseqlem4  25626  ellimc2  25785  dvcobr  25856  dvcobrOLD  25857  ply1remlem  26077  dvtaylp  26285  0cxp  26582  lgsval3  27233  lgsdinn0  27263  dchrisumlem1  27407  dchrvmasumiflem1  27419  rpvmasum2  27430  dchrvmasumlem  27441  padicabv  27548  indispconn  35228  ex-sategoelel  35415  fnejoin1  36363  ptrecube  37621  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  fdc  37746  cdlemk40f  40920  fiabv  42531  blenn0  48566