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 8441. (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  6140  axcc2lem  10347  xnegmnf  13126  rexneg  13127  xaddpnf1  13142  xaddpnf2  13143  xaddmnf1  13144  xaddmnf2  13145  mnfaddpnf  13147  rexadd  13148  fztpval  13503  sadcp1  16383  smupp1  16408  pcval  16773  ramtcl  16939  ramub1lem1  16955  xpsfrnel  17484  gexlem2  19515  frgpuptinv  19704  frgpup3lem  19710  gsummpt1n0  19898  dprdfid  19952  dpjrid  19997  sdrgacs  20736  abvtrivd  20767  znf1o  21508  znhash  21515  znunithash  21521  mplsubrg  21961  psdmul  22110  mamulid  22384  mamurid  22385  dmatid  22438  dmatmulcl  22443  scmatdmat  22458  mdetdiagid  22543  chpdmatlem2  22782  chpscmat  22785  chpidmat  22790  xkoccn  23562  iccpnfhmeo  24890  xrhmeo  24891  ioorinv2  25520  mbfi1fseqlem4  25663  ellimc2  25822  dvcobr  25891  ply1remlem  26111  dvtaylp  26318  0cxp  26615  lgsval3  27266  lgsdinn0  27296  dchrisumlem1  27440  dchrvmasumiflem1  27452  rpvmasum2  27463  dchrvmasumlem  27474  padicabv  27581  indispconn  35422  ex-sategoelel  35609  fnejoin1  36556  ptrecube  37932  poimirlem16  37948  poimirlem17  37949  poimirlem19  37951  poimirlem20  37952  fdc  38057  cdlemk40f  41356  fiabv  42980  blenn0  49007