Theorem ifnefalse 4490

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 4487 directly in this case. It happens, e.g., in oevn0 8440. (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 4487	. 2 ⊢ (¬ 𝐴 = 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)
3	1, 2	sylbi 217	1 ⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)

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

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 4479

This theorem is referenced by:  xpima2  6137  axcc2lem  10349  xnegmnf  13130  rexneg  13131  xaddpnf1  13146  xaddpnf2  13147  xaddmnf1  13148  xaddmnf2  13149  mnfaddpnf  13151  rexadd  13152  fztpval  13507  sadcp1  16384  smupp1  16409  pcval  16774  ramtcl  16940  ramub1lem1  16956  xpsfrnel  17484  gexlem2  19479  frgpuptinv  19668  frgpup3lem  19674  gsummpt1n0  19862  dprdfid  19916  dpjrid  19961  sdrgacs  20704  abvtrivd  20735  znf1o  21476  znhash  21483  znunithash  21489  mplsubrg  21930  psdmul  22069  mamulid  22344  mamurid  22345  dmatid  22398  dmatmulcl  22403  scmatdmat  22418  mdetdiagid  22503  chpdmatlem2  22742  chpscmat  22745  chpidmat  22750  xkoccn  23522  iccpnfhmeo  24859  xrhmeo  24860  ioorinv2  25492  mbfi1fseqlem4  25635  ellimc2  25794  dvcobr  25865  dvcobrOLD  25866  ply1remlem  26086  dvtaylp  26294  0cxp  26591  lgsval3  27242  lgsdinn0  27272  dchrisumlem1  27416  dchrvmasumiflem1  27428  rpvmasum2  27439  dchrvmasumlem  27450  padicabv  27557  indispconn  35206  ex-sategoelel  35393  fnejoin1  36341  ptrecube  37599  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  fdc  37724  cdlemk40f  40898  fiabv  42509  blenn0  48546