Theorem ifnefalse 4560

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-if 4549

This theorem is referenced by:  xpima2  6215  axcc2lem  10505  xnegmnf  13272  rexneg  13273  xaddpnf1  13288  xaddpnf2  13289  xaddmnf1  13290  xaddmnf2  13291  mnfaddpnf  13293  rexadd  13294  fztpval  13646  sadcp1  16501  smupp1  16526  pcval  16891  ramtcl  17057  ramub1lem1  17073  xpsfrnel  17622  gexlem2  19624  frgpuptinv  19813  frgpup3lem  19819  gsummpt1n0  20007  dprdfid  20061  dpjrid  20106  sdrgacs  20824  abvtrivd  20855  znf1o  21593  znhash  21600  znunithash  21606  mplsubrg  22048  psdmul  22193  mamulid  22468  mamurid  22469  dmatid  22522  dmatmulcl  22527  scmatdmat  22542  mdetdiagid  22627  chpdmatlem2  22866  chpscmat  22869  chpidmat  22874  xkoccn  23648  iccpnfhmeo  24995  xrhmeo  24996  ioorinv2  25629  mbfi1fseqlem4  25773  ellimc2  25932  dvcobr  26003  dvcobrOLD  26004  ply1remlem  26224  dvtaylp  26430  0cxp  26726  lgsval3  27377  lgsdinn0  27407  dchrisumlem1  27551  dchrvmasumiflem1  27563  rpvmasum2  27574  dchrvmasumlem  27585  padicabv  27692  indispconn  35202  ex-sategoelel  35389  fnejoin1  36334  ptrecube  37580  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  fdc  37705  cdlemk40f  40876  fiabv  42491  blenn0  48307