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

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

Proof of Theorem ifnefalse
StepHypRef Expression
1 df-ne 2941 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 iffalse 4499 . 2 𝐴 = 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)
31, 2sylbi 216 1 (𝐴𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2940  ifcif 4490
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2941  df-if 4491
This theorem is referenced by:  xpima2  6140  axcc2lem  10380  xnegmnf  13138  rexneg  13139  xaddpnf1  13154  xaddpnf2  13155  xaddmnf1  13156  xaddmnf2  13157  mnfaddpnf  13159  rexadd  13160  fztpval  13512  sadcp1  16343  smupp1  16368  pcval  16724  ramtcl  16890  ramub1lem1  16906  xpsfrnel  17452  gexlem2  19372  frgpuptinv  19561  frgpup3lem  19567  gsummpt1n0  19750  dprdfid  19804  dpjrid  19849  sdrgacs  20311  abvtrivd  20342  znf1o  20981  znhash  20988  znunithash  20994  mplsubrg  21434  mamulid  21813  mamurid  21814  dmatid  21867  dmatmulcl  21872  scmatdmat  21887  mdetdiagid  21972  chpdmatlem2  22211  chpscmat  22214  chpidmat  22219  xkoccn  22993  iccpnfhmeo  24331  xrhmeo  24332  ioorinv2  24962  mbfi1fseqlem4  25106  ellimc2  25264  dvcobr  25333  ply1remlem  25550  dvtaylp  25752  0cxp  26044  lgsval3  26686  lgsdinn0  26716  dchrisumlem1  26860  dchrvmasumiflem1  26872  rpvmasum2  26883  dchrvmasumlem  26894  padicabv  27001  indispconn  33892  ex-sategoelel  34079  fnejoin1  34893  ptrecube  36128  poimirlem16  36144  poimirlem17  36145  poimirlem19  36147  poimirlem20  36148  fdc  36254  cdlemk40f  39432  blenn0  46749
  Copyright terms: Public domain W3C validator