Theorem ifnefalse 4435

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2951  ifcif 4423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ne 2952  df-if 4424

This theorem is referenced by:  xpima2  6018  axcc2lem  9909  xnegmnf  12657  rexneg  12658  xaddpnf1  12673  xaddpnf2  12674  xaddmnf1  12675  xaddmnf2  12676  mnfaddpnf  12678  rexadd  12679  fztpval  13031  sadcp1  15867  smupp1  15892  pcval  16249  ramtcl  16414  ramub1lem1  16430  xpsfrnel  16906  gexlem2  18787  frgpuptinv  18977  frgpup3lem  18983  gsummpt1n0  19166  dprdfid  19220  dpjrid  19265  sdrgacs  19661  abvtrivd  19692  znf1o  20332  znhash  20339  znunithash  20345  mplsubrg  20783  mamulid  21154  mamurid  21155  dmatid  21208  dmatmulcl  21213  scmatdmat  21228  mdetdiagid  21313  chpdmatlem2  21552  chpscmat  21555  chpidmat  21560  xkoccn  22332  iccpnfhmeo  23659  xrhmeo  23660  ioorinv2  24288  mbfi1fseqlem4  24431  ellimc2  24589  dvcobr  24658  ply1remlem  24875  dvtaylp  25077  0cxp  25369  lgsval3  26011  lgsdinn0  26041  dchrisumlem1  26185  dchrvmasumiflem1  26197  rpvmasum2  26208  dchrvmasumlem  26219  padicabv  26326  indispconn  32724  ex-sategoelel  32911  fnejoin1  34140  ptrecube  35371  poimirlem16  35387  poimirlem17  35388  poimirlem19  35390  poimirlem20  35391  fdc  35497  cdlemk40f  38529  blenn0  45401