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 8484. (Contributed by David A. Wheeler, 15-May-2015.)

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1561   ≠ wne 2958  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-if 4482

This theorem is referenced by:  xpima2  6170  axcc2lem  10404  xnegmnf  13223  rexneg  13224  xaddpnf1  13239  xaddpnf2  13240  xaddmnf1  13241  xaddmnf2  13242  mnfaddpnf  13244  rexadd  13245  fztpval  13601  sadcp1  16499  smupp1  16524  pcval  16890  ramtcl  17056  ramub1lem1  17072  xpsfrnel  17602  gexlem2  19632  frgpuptinv  19821  frgpup3lem  19827  gsummpt1n0  20015  dprdfid  20069  dpjrid  20114  sdrgacs  20857  abvtrivd  20888  znf1o  21610  znhash  21617  znunithash  21623  mplsubrg  22063  psdmul  22238  mamulid  22508  mamurid  22509  dmatid  22562  dmatmulcl  22567  scmatdmat  22582  mdetdiagid  22667  chpdmatlem2  22906  chpscmat  22909  chpidmat  22914  xkoccn  23686  iccpnfhmeo  25014  xrhmeo  25015  ioorinv2  25644  mbfi1fseqlem4  25787  ellimc2  25946  dvcobr  26015  ply1remlem  26232  dvtaylp  26440  0cxp  26738  lgsval3  27386  lgsdinn0  27416  dchrisumlem1  27560  dchrvmasumiflem1  27572  rpvmasum2  27583  dchrvmasumlem  27594  padicabv  27701  indispconn  35589  ex-sategoelel  35776  fnejoin1  36733  ptrecube  38124  poimirlem16  38140  poimirlem17  38141  poimirlem19  38143  poimirlem20  38144  fdc  38249  cdlemk40f  41548  fiabv  43159  blenn0  49186