Theorem ifnefalse 4492

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933  ifcif 4480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-if 4481

This theorem is referenced by:  xpima2  6143  axcc2lem  10351  xnegmnf  13130  rexneg  13131  xaddpnf1  13146  xaddpnf2  13147  xaddmnf1  13148  xaddmnf2  13149  mnfaddpnf  13151  rexadd  13152  fztpval  13507  sadcp1  16387  smupp1  16412  pcval  16777  ramtcl  16943  ramub1lem1  16959  xpsfrnel  17488  gexlem2  19516  frgpuptinv  19705  frgpup3lem  19711  gsummpt1n0  19899  dprdfid  19953  dpjrid  19998  sdrgacs  20739  abvtrivd  20770  znf1o  21511  znhash  21518  znunithash  21524  mplsubrg  21965  psdmul  22114  mamulid  22390  mamurid  22391  dmatid  22444  dmatmulcl  22449  scmatdmat  22464  mdetdiagid  22549  chpdmatlem2  22788  chpscmat  22791  chpidmat  22796  xkoccn  23568  iccpnfhmeo  24904  xrhmeo  24905  ioorinv2  25537  mbfi1fseqlem4  25680  ellimc2  25839  dvcobr  25910  dvcobrOLD  25911  ply1remlem  26131  dvtaylp  26339  0cxp  26636  lgsval3  27287  lgsdinn0  27317  dchrisumlem1  27461  dchrvmasumiflem1  27473  rpvmasum2  27484  dchrvmasumlem  27495  padicabv  27602  indispconn  35441  ex-sategoelel  35628  fnejoin1  36575  ptrecube  37834  poimirlem16  37850  poimirlem17  37851  poimirlem19  37853  poimirlem20  37854  fdc  37959  cdlemk40f  41258  fiabv  42869  blenn0  48896