Theorem ifnefalse 4468

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2942  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-if 4457

This theorem is referenced by:  xpima2  6076  axcc2lem  10123  xnegmnf  12873  rexneg  12874  xaddpnf1  12889  xaddpnf2  12890  xaddmnf1  12891  xaddmnf2  12892  mnfaddpnf  12894  rexadd  12895  fztpval  13247  sadcp1  16090  smupp1  16115  pcval  16473  ramtcl  16639  ramub1lem1  16655  xpsfrnel  17190  gexlem2  19102  frgpuptinv  19292  frgpup3lem  19298  gsummpt1n0  19481  dprdfid  19535  dpjrid  19580  sdrgacs  19984  abvtrivd  20015  znf1o  20671  znhash  20678  znunithash  20684  mplsubrg  21121  mamulid  21498  mamurid  21499  dmatid  21552  dmatmulcl  21557  scmatdmat  21572  mdetdiagid  21657  chpdmatlem2  21896  chpscmat  21899  chpidmat  21904  xkoccn  22678  iccpnfhmeo  24014  xrhmeo  24015  ioorinv2  24644  mbfi1fseqlem4  24788  ellimc2  24946  dvcobr  25015  ply1remlem  25232  dvtaylp  25434  0cxp  25726  lgsval3  26368  lgsdinn0  26398  dchrisumlem1  26542  dchrvmasumiflem1  26554  rpvmasum2  26565  dchrvmasumlem  26576  padicabv  26683  indispconn  33096  ex-sategoelel  33283  fnejoin1  34484  ptrecube  35704  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  fdc  35830  cdlemk40f  38860  blenn0  45807