Theorem ifnefalse 4541

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ≠ wne 2930  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2931  df-if 4530

This theorem is referenced by:  xpima2  6188  axcc2lem  10459  xnegmnf  13221  rexneg  13222  xaddpnf1  13237  xaddpnf2  13238  xaddmnf1  13239  xaddmnf2  13240  mnfaddpnf  13242  rexadd  13243  fztpval  13595  sadcp1  16429  smupp1  16454  pcval  16812  ramtcl  16978  ramub1lem1  16994  xpsfrnel  17543  gexlem2  19541  frgpuptinv  19730  frgpup3lem  19736  gsummpt1n0  19924  dprdfid  19978  dpjrid  20023  sdrgacs  20693  abvtrivd  20724  znf1o  21489  znhash  21496  znunithash  21502  mplsubrg  21954  psdmul  22098  mamulid  22373  mamurid  22374  dmatid  22427  dmatmulcl  22432  scmatdmat  22447  mdetdiagid  22532  chpdmatlem2  22771  chpscmat  22774  chpidmat  22779  xkoccn  23553  iccpnfhmeo  24900  xrhmeo  24901  ioorinv2  25534  mbfi1fseqlem4  25678  ellimc2  25836  dvcobr  25907  dvcobrOLD  25908  ply1remlem  26129  dvtaylp  26335  0cxp  26630  lgsval3  27278  lgsdinn0  27308  dchrisumlem1  27452  dchrvmasumiflem1  27464  rpvmasum2  27475  dchrvmasumlem  27486  padicabv  27593  indispconn  34914  ex-sategoelel  35101  fnejoin1  35922  ptrecube  37163  poimirlem16  37179  poimirlem17  37180  poimirlem19  37182  poimirlem20  37183  fdc  37288  cdlemk40f  40461  blenn0  47758