Theorem ifnefalse 4498

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

Assertion

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

Proof of Theorem ifnefalse

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ≠ wne 2957  ifcif 4486

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-if 4487

This theorem is used by:  xpima2  6181  axcc2lem  10426  xnegmnf  13242  rexneg  13243  xaddpnf1  13258  xaddpnf2  13259  xaddmnf1  13260  xaddmnf2  13261  mnfaddpnf  13263  rexadd  13264  fztpval  13621  sadcp1  16519  smupp1  16544  pcval  16910  ramtcl  17076  ramub1lem1  17092  xpsfrnel  17622  gexlem2  19658  frgpuptinv  19847  frgpup3lem  19853  gsummpt1n0  20041  dprdfid  20095  dpjrid  20140  sdrgacs  20915  abvtrivd  20946  znf1o  21712  znhash  21719  znunithash  21725  mplsubrg  22165  psdmul  22340  mamulid  22609  mamurid  22610  dmatid  22663  dmatmulcl  22668  scmatdmat  22683  mdetdiagid  22768  chpdmatlem2  23007  chpscmat  23010  chpidmat  23015  xkoccn  23787  iccpnfhmeo  25115  xrhmeo  25116  ioorinv2  25745  mbfi1fseqlem4  25888  ellimc2  26047  dvcobr  26116  ply1remlem  26333  dvtaylp  26544  0cxp  26842  lgsval3  27490  lgsdinn0  27520  dchrisumlem1  27664  dchrvmasumiflem1  27676  rpvmasum2  27687  dchrvmasumlem  27698  padicabv  27805  indispconn  35734  ex-sategoelel  35921  fnejoin1  36907  ptrecube  38299  poimirlem16  38315  poimirlem17  38316  poimirlem19  38318  poimirlem20  38319  fdc  38424  cdlemk40f  41721  fiabv  43332  blenn0  49381