Theorem ifnefalse 4048

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ne 2782  df-if 4037

This theorem is referenced by:  xpima2  5497  axcc2lem  9141  xnegmnf  11915  rexneg  11916  xaddpnf1  11931  xaddpnf2  11932  xaddmnf1  11933  xaddmnf2  11934  mnfaddpnf  11936  rexadd  11937  fztpval  12272  sadcp1  15015  smupp1  15040  pcval  15387  ramtcl  15552  ramub1lem1  15568  xpscfv  16045  xpsfrnel  16046  gexlem2  17820  frgpuptinv  18007  frgpup3lem  18013  gsummpt1n0  18187  dprdfid  18239  dpjrid  18284  abvtrivd  18663  mplsubrg  19261  znf1o  19719  znhash  19726  znunithash  19732  mamulid  20066  mamurid  20067  dmatid  20120  dmatmulcl  20125  scmatdmat  20140  mdetdiagid  20225  chpdmatlem2  20463  chpscmat  20466  chpidmat  20471  xkoccn  21232  iccpnfhmeo  22552  xrhmeo  22553  ioorinv2  23149  mbfi1fseqlem4  23291  ellimc2  23447  dvcobr  23515  ply1remlem  23726  dvtaylp  23928  0cxp  24212  lgsval3  24840  lgsdinn0  24870  dchrisumlem1  24978  dchrvmasumiflem1  24990  rpvmasum2  25001  dchrvmasumlem  25012  padicabv  25119  indispcon  30470  fnejoin1  31533  ptrecube  32579  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  fdc  32711  cdlemk40f  35225  sdrgacs  36790  blenn0  42165