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 8443. (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  6142  axcc2lem  10349  xnegmnf  13153  rexneg  13154  xaddpnf1  13169  xaddpnf2  13170  xaddmnf1  13171  xaddmnf2  13172  mnfaddpnf  13174  rexadd  13175  fztpval  13531  sadcp1  16415  smupp1  16440  pcval  16806  ramtcl  16972  ramub1lem1  16988  xpsfrnel  17517  gexlem2  19548  frgpuptinv  19737  frgpup3lem  19743  gsummpt1n0  19931  dprdfid  19985  dpjrid  20030  sdrgacs  20769  abvtrivd  20800  znf1o  21541  znhash  21548  znunithash  21554  mplsubrg  21993  psdmul  22142  mamulid  22416  mamurid  22417  dmatid  22470  dmatmulcl  22475  scmatdmat  22490  mdetdiagid  22575  chpdmatlem2  22814  chpscmat  22817  chpidmat  22822  xkoccn  23594  iccpnfhmeo  24922  xrhmeo  24923  ioorinv2  25552  mbfi1fseqlem4  25695  ellimc2  25854  dvcobr  25923  ply1remlem  26140  dvtaylp  26347  0cxp  26643  lgsval3  27292  lgsdinn0  27322  dchrisumlem1  27466  dchrvmasumiflem1  27478  rpvmasum2  27489  dchrvmasumlem  27500  padicabv  27607  indispconn  35432  ex-sategoelel  35619  fnejoin1  36566  ptrecube  37955  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  fdc  38080  cdlemk40f  41379  fiabv  42995  blenn0  49061