Theorem ifnefalse 4471

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2943  ifcif 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-if 4460

This theorem is referenced by:  xpima2  6087  axcc2lem  10192  xnegmnf  12944  rexneg  12945  xaddpnf1  12960  xaddpnf2  12961  xaddmnf1  12962  xaddmnf2  12963  mnfaddpnf  12965  rexadd  12966  fztpval  13318  sadcp1  16162  smupp1  16187  pcval  16545  ramtcl  16711  ramub1lem1  16727  xpsfrnel  17273  gexlem2  19187  frgpuptinv  19377  frgpup3lem  19383  gsummpt1n0  19566  dprdfid  19620  dpjrid  19665  sdrgacs  20069  abvtrivd  20100  znf1o  20759  znhash  20766  znunithash  20772  mplsubrg  21211  mamulid  21590  mamurid  21591  dmatid  21644  dmatmulcl  21649  scmatdmat  21664  mdetdiagid  21749  chpdmatlem2  21988  chpscmat  21991  chpidmat  21996  xkoccn  22770  iccpnfhmeo  24108  xrhmeo  24109  ioorinv2  24739  mbfi1fseqlem4  24883  ellimc2  25041  dvcobr  25110  ply1remlem  25327  dvtaylp  25529  0cxp  25821  lgsval3  26463  lgsdinn0  26493  dchrisumlem1  26637  dchrvmasumiflem1  26649  rpvmasum2  26660  dchrvmasumlem  26671  padicabv  26778  indispconn  33196  ex-sategoelel  33383  fnejoin1  34557  ptrecube  35777  poimirlem16  35793  poimirlem17  35794  poimirlem19  35796  poimirlem20  35797  fdc  35903  cdlemk40f  38933  blenn0  45919