Theorem ifnefalse 4537

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2940  ifcif 4525

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-if 4526

This theorem is referenced by:  xpima2  6204  axcc2lem  10476  xnegmnf  13252  rexneg  13253  xaddpnf1  13268  xaddpnf2  13269  xaddmnf1  13270  xaddmnf2  13271  mnfaddpnf  13273  rexadd  13274  fztpval  13626  sadcp1  16492  smupp1  16517  pcval  16882  ramtcl  17048  ramub1lem1  17064  xpsfrnel  17607  gexlem2  19600  frgpuptinv  19789  frgpup3lem  19795  gsummpt1n0  19983  dprdfid  20037  dpjrid  20082  sdrgacs  20802  abvtrivd  20833  znf1o  21570  znhash  21577  znunithash  21583  mplsubrg  22025  psdmul  22170  mamulid  22447  mamurid  22448  dmatid  22501  dmatmulcl  22506  scmatdmat  22521  mdetdiagid  22606  chpdmatlem2  22845  chpscmat  22848  chpidmat  22853  xkoccn  23627  iccpnfhmeo  24976  xrhmeo  24977  ioorinv2  25610  mbfi1fseqlem4  25753  ellimc2  25912  dvcobr  25983  dvcobrOLD  25984  ply1remlem  26204  dvtaylp  26412  0cxp  26708  lgsval3  27359  lgsdinn0  27389  dchrisumlem1  27533  dchrvmasumiflem1  27545  rpvmasum2  27556  dchrvmasumlem  27567  padicabv  27674  indispconn  35239  ex-sategoelel  35426  fnejoin1  36369  ptrecube  37627  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  fdc  37752  cdlemk40f  40921  fiabv  42546  blenn0  48494