Theorem ifnefalse 4492

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933  ifcif 4480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-if 4481

This theorem is referenced by:  xpima2  6143  axcc2lem  10350  xnegmnf  13129  rexneg  13130  xaddpnf1  13145  xaddpnf2  13146  xaddmnf1  13147  xaddmnf2  13148  mnfaddpnf  13150  rexadd  13151  fztpval  13506  sadcp1  16386  smupp1  16411  pcval  16776  ramtcl  16942  ramub1lem1  16958  xpsfrnel  17487  gexlem2  19515  frgpuptinv  19704  frgpup3lem  19710  gsummpt1n0  19898  dprdfid  19952  dpjrid  19997  sdrgacs  20738  abvtrivd  20769  znf1o  21510  znhash  21517  znunithash  21523  mplsubrg  21964  psdmul  22113  mamulid  22389  mamurid  22390  dmatid  22443  dmatmulcl  22448  scmatdmat  22463  mdetdiagid  22548  chpdmatlem2  22787  chpscmat  22790  chpidmat  22795  xkoccn  23567  iccpnfhmeo  24903  xrhmeo  24904  ioorinv2  25536  mbfi1fseqlem4  25679  ellimc2  25838  dvcobr  25909  dvcobrOLD  25910  ply1remlem  26130  dvtaylp  26338  0cxp  26635  lgsval3  27286  lgsdinn0  27316  dchrisumlem1  27460  dchrvmasumiflem1  27472  rpvmasum2  27483  dchrvmasumlem  27494  padicabv  27601  indispconn  35409  ex-sategoelel  35596  fnejoin1  36543  ptrecube  37792  poimirlem16  37808  poimirlem17  37809  poimirlem19  37811  poimirlem20  37812  fdc  37917  cdlemk40f  41216  fiabv  42827  blenn0  48855