Theorem ifnefalse 4493

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

Assertion

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

Proof of Theorem ifnefalse

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ≠ wne 2955  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-if 4482

This theorem is used by:  xpima2  6175  axcc2lem  10514  xnegmnf  13340  rexneg  13341  xaddpnf1  13356  xaddpnf2  13357  xaddmnf1  13358  xaddmnf2  13359  mnfaddpnf  13361  rexadd  13362  fztpval  13720  sadcp1  16625  smupp1  16650  pcval  17022  ramtcl  17188  ramub1lem1  17204  xpsfrnel  17734  gexlem2  19796  frgpuptinv  19985  frgpup3lem  19991  gsummpt1n0  20179  dprdfid  20233  dpjrid  20278  sdrgacs  21058  abvtrivd  21089  znf1o  21857  znhash  21864  znunithash  21870  mplsubrg  22312  psdmul  22487  mamulid  22756  mamurid  22757  dmatid  22810  dmatmulcl  22815  scmatdmat  22830  mdetdiagid  22915  chpdmatlem2  23157  chpscmat  23160  chpidmat  23165  xkoccn  23938  iccpnfhmeo  25266  xrhmeo  25267  ioorinv2  25896  mbfi1fseqlem4  26039  ellimc2  26197  dvcobr  26266  ply1remlem  26483  dvtaylp  26697  0cxp  26994  lgsval3  27642  lgsdinn0  27672  dchrisumlem1  27816  dchrvmasumiflem1  27828  rpvmasum2  27839  dchrvmasumlem  27850  padicabv  27957  indispconn  36041  ex-sategoelel  36228  fnejoin1  37198  ptrecube  38581  poimirlem16  38597  poimirlem17  38598  poimirlem19  38600  poimirlem20  38601  fdc  38722  cdlemk40f  42019  fiabv  43643  blenn0  49728