Theorem ifnefalse 4478

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ≠ wne 3016  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-ne 3017  df-if 4467

This theorem is referenced by:  xpima2  6035  axcc2lem  9852  xnegmnf  12597  rexneg  12598  xaddpnf1  12613  xaddpnf2  12614  xaddmnf1  12615  xaddmnf2  12616  mnfaddpnf  12618  rexadd  12619  fztpval  12963  sadcp1  15798  smupp1  15823  pcval  16175  ramtcl  16340  ramub1lem1  16356  xpsfrnel  16829  gexlem2  18701  frgpuptinv  18891  frgpup3lem  18897  gsummpt1n0  19079  dprdfid  19133  dpjrid  19178  sdrgacs  19574  abvtrivd  19605  mplsubrg  20214  znf1o  20692  znhash  20699  znunithash  20705  mamulid  21044  mamurid  21045  dmatid  21098  dmatmulcl  21103  scmatdmat  21118  mdetdiagid  21203  chpdmatlem2  21441  chpscmat  21444  chpidmat  21449  xkoccn  22221  iccpnfhmeo  23543  xrhmeo  23544  ioorinv2  24170  mbfi1fseqlem4  24313  ellimc2  24469  dvcobr  24537  ply1remlem  24750  dvtaylp  24952  0cxp  25243  lgsval3  25885  lgsdinn0  25915  dchrisumlem1  26059  dchrvmasumiflem1  26071  rpvmasum2  26082  dchrvmasumlem  26093  padicabv  26200  indispconn  32476  ex-sategoelel  32663  fnejoin1  33711  ptrecube  34886  poimirlem16  34902  poimirlem17  34903  poimirlem19  34905  poimirlem20  34906  fdc  35014  cdlemk40f  38049  blenn0  44627