Theorem ifnefalse 4493

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

Assertion

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

Proof of Theorem ifnefalse

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2955  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-if 4482

This theorem is used by:  xpima2  6171  axcc2lem  10485  xnegmnf  13309  rexneg  13310  xaddpnf1  13325  xaddpnf2  13326  xaddmnf1  13327  xaddmnf2  13328  mnfaddpnf  13330  rexadd  13331  fztpval  13688  sadcp1  16592  smupp1  16617  pcval  16983  ramtcl  17149  ramub1lem1  17165  xpsfrnel  17695  gexlem2  19757  frgpuptinv  19946  frgpup3lem  19952  gsummpt1n0  20140  dprdfid  20194  dpjrid  20239  sdrgacs  21019  abvtrivd  21050  znf1o  21818  znhash  21825  znunithash  21831  mplsubrg  22273  psdmul  22448  mamulid  22717  mamurid  22718  dmatid  22771  dmatmulcl  22776  scmatdmat  22791  mdetdiagid  22876  chpdmatlem2  23118  chpscmat  23121  chpidmat  23126  xkoccn  23899  iccpnfhmeo  25227  xrhmeo  25228  ioorinv2  25857  mbfi1fseqlem4  26000  ellimc2  26158  dvcobr  26227  ply1remlem  26444  dvtaylp  26660  0cxp  26957  lgsval3  27605  lgsdinn0  27635  dchrisumlem1  27779  dchrvmasumiflem1  27791  rpvmasum2  27802  dchrvmasumlem  27813  padicabv  27920  indispconn  35920  ex-sategoelel  36107  fnejoin1  37078  ptrecube  38458  poimirlem16  38474  poimirlem17  38475  poimirlem19  38477  poimirlem20  38478  fdc  38599  cdlemk40f  41896  fiabv  43522  blenn0  49607