Theorem ifnefalse 4498

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1568   ≠ wne 2956  ifcif 4486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-if 4487

This theorem is referenced by:  xpima2  6182  axcc2lem  10419  xnegmnf  13235  rexneg  13236  xaddpnf1  13251  xaddpnf2  13252  xaddmnf1  13253  xaddmnf2  13254  mnfaddpnf  13256  rexadd  13257  fztpval  13613  sadcp1  16512  smupp1  16537  pcval  16903  ramtcl  17069  ramub1lem1  17085  xpsfrnel  17615  gexlem2  19651  frgpuptinv  19840  frgpup3lem  19846  gsummpt1n0  20034  dprdfid  20088  dpjrid  20133  sdrgacs  20883  abvtrivd  20914  znf1o  21680  znhash  21687  znunithash  21693  mplsubrg  22133  psdmul  22308  mamulid  22577  mamurid  22578  dmatid  22631  dmatmulcl  22636  scmatdmat  22651  mdetdiagid  22736  chpdmatlem2  22975  chpscmat  22978  chpidmat  22983  xkoccn  23755  iccpnfhmeo  25083  xrhmeo  25084  ioorinv2  25713  mbfi1fseqlem4  25856  ellimc2  26015  dvcobr  26084  ply1remlem  26301  dvtaylp  26509  0cxp  26807  lgsval3  27455  lgsdinn0  27485  dchrisumlem1  27629  dchrvmasumiflem1  27641  rpvmasum2  27652  dchrvmasumlem  27663  padicabv  27770  indispconn  35680  ex-sategoelel  35867  fnejoin1  36823  ptrecube  38215  poimirlem16  38231  poimirlem17  38232  poimirlem19  38234  poimirlem20  38235  fdc  38340  cdlemk40f  41639  fiabv  43252  blenn0  49298