Theorem ifnefalse 4539

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2938  ifcif 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-if 4528

This theorem is referenced by:  xpima2  6182  axcc2lem  10433  xnegmnf  13193  rexneg  13194  xaddpnf1  13209  xaddpnf2  13210  xaddmnf1  13211  xaddmnf2  13212  mnfaddpnf  13214  rexadd  13215  fztpval  13567  sadcp1  16400  smupp1  16425  pcval  16781  ramtcl  16947  ramub1lem1  16963  xpsfrnel  17512  gexlem2  19491  frgpuptinv  19680  frgpup3lem  19686  gsummpt1n0  19874  dprdfid  19928  dpjrid  19973  sdrgacs  20560  abvtrivd  20591  znf1o  21326  znhash  21333  znunithash  21339  mplsubrg  21783  mamulid  22163  mamurid  22164  dmatid  22217  dmatmulcl  22222  scmatdmat  22237  mdetdiagid  22322  chpdmatlem2  22561  chpscmat  22564  chpidmat  22569  xkoccn  23343  iccpnfhmeo  24690  xrhmeo  24691  ioorinv2  25324  mbfi1fseqlem4  25468  ellimc2  25626  dvcobr  25697  dvcobrOLD  25698  ply1remlem  25915  dvtaylp  26118  0cxp  26410  lgsval3  27054  lgsdinn0  27084  dchrisumlem1  27228  dchrvmasumiflem1  27240  rpvmasum2  27251  dchrvmasumlem  27262  padicabv  27369  indispconn  34523  ex-sategoelel  34710  fnejoin1  35556  ptrecube  36791  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  fdc  36916  cdlemk40f  40093  blenn0  47346