Theorem ifnefalse 4536

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534   ≠ wne 2935  ifcif 4524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ne 2936  df-if 4525

This theorem is referenced by:  xpima2  6182  axcc2lem  10451  xnegmnf  13213  rexneg  13214  xaddpnf1  13229  xaddpnf2  13230  xaddmnf1  13231  xaddmnf2  13232  mnfaddpnf  13234  rexadd  13235  fztpval  13587  sadcp1  16421  smupp1  16446  pcval  16804  ramtcl  16970  ramub1lem1  16986  xpsfrnel  17535  gexlem2  19528  frgpuptinv  19717  frgpup3lem  19723  gsummpt1n0  19911  dprdfid  19965  dpjrid  20010  sdrgacs  20678  abvtrivd  20709  znf1o  21472  znhash  21479  znunithash  21485  mplsubrg  21934  psdmul  22077  mamulid  22330  mamurid  22331  dmatid  22384  dmatmulcl  22389  scmatdmat  22404  mdetdiagid  22489  chpdmatlem2  22728  chpscmat  22731  chpidmat  22736  xkoccn  23510  iccpnfhmeo  24857  xrhmeo  24858  ioorinv2  25491  mbfi1fseqlem4  25635  ellimc2  25793  dvcobr  25864  dvcobrOLD  25865  ply1remlem  26086  dvtaylp  26292  0cxp  26587  lgsval3  27235  lgsdinn0  27265  dchrisumlem1  27409  dchrvmasumiflem1  27421  rpvmasum2  27432  dchrvmasumlem  27443  padicabv  27550  indispconn  34780  ex-sategoelel  34967  fnejoin1  35788  ptrecube  37028  poimirlem16  37044  poimirlem17  37045  poimirlem19  37047  poimirlem20  37048  fdc  37153  cdlemk40f  40329  blenn0  47569