Theorem ifnefalse 4238

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1631   ≠ wne 2943  ifcif 4226

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-ne 2944  df-if 4227

This theorem is referenced by:  xpima2  5718  axcc2lem  9464  xnegmnf  12246  rexneg  12247  xaddpnf1  12262  xaddpnf2  12263  xaddmnf1  12264  xaddmnf2  12265  mnfaddpnf  12267  rexadd  12268  fztpval  12609  sadcp1  15385  smupp1  15410  pcval  15756  ramtcl  15921  ramub1lem1  15937  xpscfv  16430  xpsfrnel  16431  gexlem2  18204  frgpuptinv  18391  frgpup3lem  18397  gsummpt1n0  18571  dprdfid  18624  dpjrid  18669  abvtrivd  19050  mplsubrg  19655  znf1o  20115  znhash  20122  znunithash  20128  mamulid  20464  mamurid  20465  dmatid  20519  dmatmulcl  20524  scmatdmat  20539  mdetdiagid  20624  chpdmatlem2  20864  chpscmat  20867  chpidmat  20872  xkoccn  21643  iccpnfhmeo  22964  xrhmeo  22965  ioorinv2  23563  mbfi1fseqlem4  23705  ellimc2  23861  dvcobr  23929  ply1remlem  24142  dvtaylp  24344  0cxp  24633  lgsval3  25261  lgsdinn0  25291  dchrisumlem1  25399  dchrvmasumiflem1  25411  rpvmasum2  25422  dchrvmasumlem  25433  padicabv  25540  indispconn  31554  fnejoin1  32700  ptrecube  33742  poimirlem16  33758  poimirlem17  33759  poimirlem19  33761  poimirlem20  33762  fdc  33873  cdlemk40f  36729  sdrgacs  38297  blenn0  42892