Theorem ifnefalse 4397

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1522   ≠ wne 2984  ifcif 4385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1762  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-ne 2985  df-if 4386

This theorem is referenced by:  xpima2  5922  axcc2lem  9709  xnegmnf  12458  rexneg  12459  xaddpnf1  12474  xaddpnf2  12475  xaddmnf1  12476  xaddmnf2  12477  mnfaddpnf  12479  rexadd  12480  fztpval  12824  sadcp1  15642  smupp1  15667  pcval  16015  ramtcl  16180  ramub1lem1  16196  xpsfrnel  16669  gexlem2  18442  frgpuptinv  18629  frgpup3lem  18635  gsummpt1n0  18810  dprdfid  18861  dpjrid  18906  sdrgacs  19275  abvtrivd  19306  mplsubrg  19913  znf1o  20385  znhash  20392  znunithash  20398  mamulid  20739  mamurid  20740  dmatid  20793  dmatmulcl  20798  scmatdmat  20813  mdetdiagid  20898  chpdmatlem2  21136  chpscmat  21139  chpidmat  21144  xkoccn  21916  iccpnfhmeo  23237  xrhmeo  23238  ioorinv2  23864  mbfi1fseqlem4  24007  ellimc2  24163  dvcobr  24231  ply1remlem  24444  dvtaylp  24646  0cxp  24935  lgsval3  25578  lgsdinn0  25608  dchrisumlem1  25752  dchrvmasumiflem1  25764  rpvmasum2  25775  dchrvmasumlem  25786  padicabv  25893  indispconn  32095  ex-sategoelel  32282  fnejoin1  33331  ptrecube  34448  poimirlem16  34464  poimirlem17  34465  poimirlem19  34467  poimirlem20  34468  fdc  34577  cdlemk40f  37611  blenn0  44140