Theorem ifnefalse 4468

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2930  ifcif 4456

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ne 2931  df-if 4457

This theorem is referenced by:  xpima2  6137  axcc2lem  10347  xnegmnf  13151  rexneg  13152  xaddpnf1  13167  xaddpnf2  13168  xaddmnf1  13169  xaddmnf2  13170  mnfaddpnf  13172  rexadd  13173  fztpval  13529  sadcp1  16413  smupp1  16438  pcval  16804  ramtcl  16970  ramub1lem1  16986  xpsfrnel  17515  gexlem2  19546  frgpuptinv  19735  frgpup3lem  19741  gsummpt1n0  19929  dprdfid  19983  dpjrid  20028  sdrgacs  20767  abvtrivd  20798  znf1o  21520  znhash  21527  znunithash  21533  mplsubrg  21972  psdmul  22121  mamulid  22394  mamurid  22395  dmatid  22448  dmatmulcl  22453  scmatdmat  22468  mdetdiagid  22553  chpdmatlem2  22792  chpscmat  22795  chpidmat  22800  xkoccn  23572  iccpnfhmeo  24900  xrhmeo  24901  ioorinv2  25530  mbfi1fseqlem4  25673  ellimc2  25832  dvcobr  25901  ply1remlem  26118  dvtaylp  26323  0cxp  26618  lgsval3  27266  lgsdinn0  27296  dchrisumlem1  27440  dchrvmasumiflem1  27452  rpvmasum2  27463  dchrvmasumlem  27474  padicabv  27581  indispconn  35404  ex-sategoelel  35591  fnejoin1  36538  ptrecube  37929  poimirlem16  37945  poimirlem17  37946  poimirlem19  37948  poimirlem20  37949  fdc  38054  cdlemk40f  41353  fiabv  42969  blenn0  49037