Theorem ifnefalse 4482

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1550   ≠ wne 2947  ifcif 4470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ne 2948  df-if 4471

This theorem is referenced by:  xpima2  6155  axcc2lem  10379  xnegmnf  13199  rexneg  13200  xaddpnf1  13215  xaddpnf2  13216  xaddmnf1  13217  xaddmnf2  13218  mnfaddpnf  13220  rexadd  13221  fztpval  13577  sadcp1  16461  smupp1  16486  pcval  16852  ramtcl  17018  ramub1lem1  17034  xpsfrnel  17564  gexlem2  19594  frgpuptinv  19783  frgpup3lem  19789  gsummpt1n0  19977  dprdfid  20031  dpjrid  20076  sdrgacs  20819  abvtrivd  20850  znf1o  21572  znhash  21579  znunithash  21585  mplsubrg  22025  psdmul  22200  mamulid  22470  mamurid  22471  dmatid  22524  dmatmulcl  22529  scmatdmat  22544  mdetdiagid  22629  chpdmatlem2  22868  chpscmat  22871  chpidmat  22876  xkoccn  23648  iccpnfhmeo  24976  xrhmeo  24977  ioorinv2  25606  mbfi1fseqlem4  25749  ellimc2  25908  dvcobr  25977  ply1remlem  26194  dvtaylp  26399  0cxp  26697  lgsval3  27345  lgsdinn0  27375  dchrisumlem1  27519  dchrvmasumiflem1  27531  rpvmasum2  27542  dchrvmasumlem  27553  padicabv  27660  indispconn  35522  ex-sategoelel  35709  fnejoin1  36666  ptrecube  38057  poimirlem16  38073  poimirlem17  38074  poimirlem19  38076  poimirlem20  38077  fdc  38182  cdlemk40f  41481  fiabv  43092  blenn0  49133