Theorem ifnefalse 4543

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2938  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-if 4532

This theorem is referenced by:  xpima2  6206  axcc2lem  10474  xnegmnf  13249  rexneg  13250  xaddpnf1  13265  xaddpnf2  13266  xaddmnf1  13267  xaddmnf2  13268  mnfaddpnf  13270  rexadd  13271  fztpval  13623  sadcp1  16489  smupp1  16514  pcval  16878  ramtcl  17044  ramub1lem1  17060  xpsfrnel  17609  gexlem2  19615  frgpuptinv  19804  frgpup3lem  19810  gsummpt1n0  19998  dprdfid  20052  dpjrid  20097  sdrgacs  20819  abvtrivd  20850  znf1o  21588  znhash  21595  znunithash  21601  mplsubrg  22043  psdmul  22188  mamulid  22463  mamurid  22464  dmatid  22517  dmatmulcl  22522  scmatdmat  22537  mdetdiagid  22622  chpdmatlem2  22861  chpscmat  22864  chpidmat  22869  xkoccn  23643  iccpnfhmeo  24990  xrhmeo  24991  ioorinv2  25624  mbfi1fseqlem4  25768  ellimc2  25927  dvcobr  25998  dvcobrOLD  25999  ply1remlem  26219  dvtaylp  26427  0cxp  26723  lgsval3  27374  lgsdinn0  27404  dchrisumlem1  27548  dchrvmasumiflem1  27560  rpvmasum2  27571  dchrvmasumlem  27582  padicabv  27689  indispconn  35219  ex-sategoelel  35406  fnejoin1  36351  ptrecube  37607  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  fdc  37732  cdlemk40f  40902  fiabv  42523  blenn0  48423