Theorem ifnefalse 4497

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

Assertion

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

Proof of Theorem ifnefalse

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-if 4486

This theorem is used by:  xpima2  6188  axcc2lem  10541  xnegmnf  13367  rexneg  13368  xaddpnf1  13383  xaddpnf2  13384  xaddmnf1  13385  xaddmnf2  13386  mnfaddpnf  13388  rexadd  13389  fztpval  13747  sadcp1  16654  smupp1  16679  pcval  17051  ramtcl  17217  ramub1lem1  17233  xpsfrnel  17763  gexlem2  19826  frgpuptinv  20015  frgpup3lem  20021  gsummpt1n0  20209  dprdfid  20263  dpjrid  20308  sdrgacs  21088  abvtrivd  21119  znf1o  21887  znhash  21894  znunithash  21900  mplsubrg  22342  psdmul  22517  mamulid  22786  mamurid  22787  dmatid  22840  dmatmulcl  22845  scmatdmat  22860  mdetdiagid  22945  chpdmatlem2  23187  chpscmat  23190  chpidmat  23195  xkoccn  23968  iccpnfhmeo  25296  xrhmeo  25297  ioorinv2  25926  mbfi1fseqlem4  26069  ellimc2  26227  dvcobr  26296  ply1remlem  26513  dvtaylp  26727  0cxp  27024  lgsval3  27672  lgsdinn0  27702  dchrisumlem1  27846  dchrvmasumiflem1  27858  rpvmasum2  27869  dchrvmasumlem  27880  padicabv  27987  indispconn  36166  ex-sategoelel  36353  fnejoin1  37334  ptrecube  38730  poimirlem16  38746  poimirlem17  38747  poimirlem19  38749  poimirlem20  38750  fdc  38871  cdlemk40f  42168  fiabv  43793  blenn0  49890