Theorem ifnefalse 4479

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-if 4468

This theorem is referenced by:  xpima2  6149  axcc2lem  10358  xnegmnf  13162  rexneg  13163  xaddpnf1  13178  xaddpnf2  13179  xaddmnf1  13180  xaddmnf2  13181  mnfaddpnf  13183  rexadd  13184  fztpval  13540  sadcp1  16424  smupp1  16449  pcval  16815  ramtcl  16981  ramub1lem1  16997  xpsfrnel  17526  gexlem2  19557  frgpuptinv  19746  frgpup3lem  19752  gsummpt1n0  19940  dprdfid  19994  dpjrid  20039  sdrgacs  20778  abvtrivd  20809  znf1o  21531  znhash  21538  znunithash  21544  mplsubrg  21983  psdmul  22132  mamulid  22406  mamurid  22407  dmatid  22460  dmatmulcl  22465  scmatdmat  22480  mdetdiagid  22565  chpdmatlem2  22804  chpscmat  22807  chpidmat  22812  xkoccn  23584  iccpnfhmeo  24912  xrhmeo  24913  ioorinv2  25542  mbfi1fseqlem4  25685  ellimc2  25844  dvcobr  25913  ply1remlem  26130  dvtaylp  26335  0cxp  26630  lgsval3  27278  lgsdinn0  27308  dchrisumlem1  27452  dchrvmasumiflem1  27464  rpvmasum2  27475  dchrvmasumlem  27486  padicabv  27593  indispconn  35416  ex-sategoelel  35603  fnejoin1  36550  ptrecube  37941  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  fdc  38066  cdlemk40f  41365  fiabv  42981  blenn0  49043