Theorem ifnefalse 4486

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2928  ifcif 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-if 4475

This theorem is referenced by:  xpima2  6137  axcc2lem  10333  xnegmnf  13115  rexneg  13116  xaddpnf1  13131  xaddpnf2  13132  xaddmnf1  13133  xaddmnf2  13134  mnfaddpnf  13136  rexadd  13137  fztpval  13492  sadcp1  16372  smupp1  16397  pcval  16762  ramtcl  16928  ramub1lem1  16944  xpsfrnel  17472  gexlem2  19500  frgpuptinv  19689  frgpup3lem  19695  gsummpt1n0  19883  dprdfid  19937  dpjrid  19982  sdrgacs  20722  abvtrivd  20753  znf1o  21494  znhash  21501  znunithash  21507  mplsubrg  21948  psdmul  22087  mamulid  22362  mamurid  22363  dmatid  22416  dmatmulcl  22421  scmatdmat  22436  mdetdiagid  22521  chpdmatlem2  22760  chpscmat  22763  chpidmat  22768  xkoccn  23540  iccpnfhmeo  24876  xrhmeo  24877  ioorinv2  25509  mbfi1fseqlem4  25652  ellimc2  25811  dvcobr  25882  dvcobrOLD  25883  ply1remlem  26103  dvtaylp  26311  0cxp  26608  lgsval3  27259  lgsdinn0  27289  dchrisumlem1  27433  dchrvmasumiflem1  27445  rpvmasum2  27456  dchrvmasumlem  27467  padicabv  27574  indispconn  35285  ex-sategoelel  35472  fnejoin1  36419  ptrecube  37666  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  fdc  37791  cdlemk40f  41024  fiabv  42635  blenn0  48679