Theorem ifnefalse 4485

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2926  ifcif 4473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-if 4474

This theorem is referenced by:  xpima2  6128  axcc2lem  10319  xnegmnf  13101  rexneg  13102  xaddpnf1  13117  xaddpnf2  13118  xaddmnf1  13119  xaddmnf2  13120  mnfaddpnf  13122  rexadd  13123  fztpval  13478  sadcp1  16358  smupp1  16383  pcval  16748  ramtcl  16914  ramub1lem1  16930  xpsfrnel  17458  gexlem2  19487  frgpuptinv  19676  frgpup3lem  19682  gsummpt1n0  19870  dprdfid  19924  dpjrid  19969  sdrgacs  20709  abvtrivd  20740  znf1o  21481  znhash  21488  znunithash  21494  mplsubrg  21935  psdmul  22074  mamulid  22349  mamurid  22350  dmatid  22403  dmatmulcl  22408  scmatdmat  22423  mdetdiagid  22508  chpdmatlem2  22747  chpscmat  22750  chpidmat  22755  xkoccn  23527  iccpnfhmeo  24863  xrhmeo  24864  ioorinv2  25496  mbfi1fseqlem4  25639  ellimc2  25798  dvcobr  25869  dvcobrOLD  25870  ply1remlem  26090  dvtaylp  26298  0cxp  26595  lgsval3  27246  lgsdinn0  27276  dchrisumlem1  27420  dchrvmasumiflem1  27432  rpvmasum2  27443  dchrvmasumlem  27454  padicabv  27561  indispconn  35246  ex-sategoelel  35433  fnejoin1  36381  ptrecube  37639  poimirlem16  37655  poimirlem17  37656  poimirlem19  37658  poimirlem20  37659  fdc  37764  cdlemk40f  40937  fiabv  42548  blenn0  48584