Theorem ifnefalse 4512

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2932  ifcif 4500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-if 4501

This theorem is referenced by:  xpima2  6173  axcc2lem  10450  xnegmnf  13226  rexneg  13227  xaddpnf1  13242  xaddpnf2  13243  xaddmnf1  13244  xaddmnf2  13245  mnfaddpnf  13247  rexadd  13248  fztpval  13603  sadcp1  16474  smupp1  16499  pcval  16864  ramtcl  17030  ramub1lem1  17046  xpsfrnel  17576  gexlem2  19563  frgpuptinv  19752  frgpup3lem  19758  gsummpt1n0  19946  dprdfid  20000  dpjrid  20045  sdrgacs  20761  abvtrivd  20792  znf1o  21512  znhash  21519  znunithash  21525  mplsubrg  21965  psdmul  22104  mamulid  22379  mamurid  22380  dmatid  22433  dmatmulcl  22438  scmatdmat  22453  mdetdiagid  22538  chpdmatlem2  22777  chpscmat  22780  chpidmat  22785  xkoccn  23557  iccpnfhmeo  24894  xrhmeo  24895  ioorinv2  25528  mbfi1fseqlem4  25671  ellimc2  25830  dvcobr  25901  dvcobrOLD  25902  ply1remlem  26122  dvtaylp  26330  0cxp  26627  lgsval3  27278  lgsdinn0  27308  dchrisumlem1  27452  dchrvmasumiflem1  27464  rpvmasum2  27475  dchrvmasumlem  27486  padicabv  27593  indispconn  35256  ex-sategoelel  35443  fnejoin1  36386  ptrecube  37644  poimirlem16  37660  poimirlem17  37661  poimirlem19  37663  poimirlem20  37664  fdc  37769  cdlemk40f  40938  fiabv  42559  blenn0  48553