Theorem ifnefalse 4540

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2940  ifcif 4528

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-if 4529

This theorem is referenced by:  xpima2  6183  axcc2lem  10430  xnegmnf  13188  rexneg  13189  xaddpnf1  13204  xaddpnf2  13205  xaddmnf1  13206  xaddmnf2  13207  mnfaddpnf  13209  rexadd  13210  fztpval  13562  sadcp1  16395  smupp1  16420  pcval  16776  ramtcl  16942  ramub1lem1  16958  xpsfrnel  17507  gexlem2  19449  frgpuptinv  19638  frgpup3lem  19644  gsummpt1n0  19832  dprdfid  19886  dpjrid  19931  sdrgacs  20416  abvtrivd  20447  znf1o  21106  znhash  21113  znunithash  21119  mplsubrg  21563  mamulid  21942  mamurid  21943  dmatid  21996  dmatmulcl  22001  scmatdmat  22016  mdetdiagid  22101  chpdmatlem2  22340  chpscmat  22343  chpidmat  22348  xkoccn  23122  iccpnfhmeo  24460  xrhmeo  24461  ioorinv2  25091  mbfi1fseqlem4  25235  ellimc2  25393  dvcobr  25462  ply1remlem  25679  dvtaylp  25881  0cxp  26173  lgsval3  26815  lgsdinn0  26845  dchrisumlem1  26989  dchrvmasumiflem1  27001  rpvmasum2  27012  dchrvmasumlem  27023  padicabv  27130  indispconn  34220  ex-sategoelel  34407  gg-dvcobr  35171  fnejoin1  35248  ptrecube  36483  poimirlem16  36499  poimirlem17  36500  poimirlem19  36502  poimirlem20  36503  fdc  36608  cdlemk40f  39785  blenn0  47249