MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifnefalse Structured version   Visualization version   GIF version

Theorem ifnefalse 4131
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 4128 directly in this case. It happens, e.g., in oevn0 7640. (Contributed by David A. Wheeler, 15-May-2015.)
Assertion
Ref Expression
ifnefalse (𝐴𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)

Proof of Theorem ifnefalse
StepHypRef Expression
1 df-ne 2824 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 iffalse 4128 . 2 𝐴 = 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)
31, 2sylbi 207 1 (𝐴𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823  ifcif 4119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ne 2824  df-if 4120
This theorem is referenced by:  xpima2  5613  axcc2lem  9296  xnegmnf  12079  rexneg  12080  xaddpnf1  12095  xaddpnf2  12096  xaddmnf1  12097  xaddmnf2  12098  mnfaddpnf  12100  rexadd  12101  fztpval  12440  sadcp1  15224  smupp1  15249  pcval  15596  ramtcl  15761  ramub1lem1  15777  xpscfv  16269  xpsfrnel  16270  gexlem2  18043  frgpuptinv  18230  frgpup3lem  18236  gsummpt1n0  18410  dprdfid  18462  dpjrid  18507  abvtrivd  18888  mplsubrg  19488  znf1o  19948  znhash  19955  znunithash  19961  mamulid  20295  mamurid  20296  dmatid  20349  dmatmulcl  20354  scmatdmat  20369  mdetdiagid  20454  chpdmatlem2  20692  chpscmat  20695  chpidmat  20700  xkoccn  21470  iccpnfhmeo  22791  xrhmeo  22792  ioorinv2  23389  mbfi1fseqlem4  23530  ellimc2  23686  dvcobr  23754  ply1remlem  23967  dvtaylp  24169  0cxp  24457  lgsval3  25085  lgsdinn0  25115  dchrisumlem1  25223  dchrvmasumiflem1  25235  rpvmasum2  25246  dchrvmasumlem  25257  padicabv  25364  indispconn  31342  fnejoin1  32488  ptrecube  33539  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  fdc  33671  cdlemk40f  36524  sdrgacs  38088  blenn0  42692
  Copyright terms: Public domain W3C validator