Theorem ifnefalse 4288

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

Assertion

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

Proof of Theorem ifnefalse

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1653   ≠ wne 2970  ifcif 4276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2776

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2785  df-cleq 2791  df-clel 2794  df-ne 2971  df-if 4277

This theorem is referenced by:  xpima2  5794  axcc2lem  9545  xnegmnf  12287  rexneg  12288  xaddpnf1  12303  xaddpnf2  12304  xaddmnf1  12305  xaddmnf2  12306  mnfaddpnf  12308  rexadd  12309  fztpval  12653  sadcp1  15509  smupp1  15534  pcval  15879  ramtcl  16044  ramub1lem1  16060  xpscfv  16534  xpsfrnel  16535  gexlem2  18307  frgpuptinv  18496  frgpup3lem  18502  gsummpt1n0  18676  dprdfid  18729  dpjrid  18774  abvtrivd  19155  mplsubrg  19760  znf1o  20218  znhash  20225  znunithash  20231  mamulid  20569  mamurid  20570  dmatid  20624  dmatmulcl  20629  scmatdmat  20644  mdetdiagid  20729  chpdmatlem2  20969  chpscmat  20972  chpidmat  20977  xkoccn  21748  iccpnfhmeo  23069  xrhmeo  23070  ioorinv2  23680  mbfi1fseqlem4  23823  ellimc2  23979  dvcobr  24047  ply1remlem  24260  dvtaylp  24462  0cxp  24750  lgsval3  25389  lgsdinn0  25419  dchrisumlem1  25527  dchrvmasumiflem1  25539  rpvmasum2  25550  dchrvmasumlem  25561  padicabv  25668  indispconn  31726  fnejoin1  32868  ptrecube  33891  poimirlem16  33907  poimirlem17  33908  poimirlem19  33910  poimirlem20  33911  fdc  34021  cdlemk40f  36933  sdrgacs  38545  blenn0  43155