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

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

Proof of Theorem ifnefalse
StepHypRef Expression
1 df-ne 2797 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 iffalse 4072 . 2 𝐴 = 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)
31, 2sylbi 207 1 (𝐴𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1480  wne 2796  ifcif 4063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-ne 2797  df-if 4064
This theorem is referenced by:  xpima2  5541  axcc2lem  9203  xnegmnf  11983  rexneg  11984  xaddpnf1  11999  xaddpnf2  12000  xaddmnf1  12001  xaddmnf2  12002  mnfaddpnf  12004  rexadd  12005  fztpval  12341  sadcp1  15096  smupp1  15121  pcval  15468  ramtcl  15633  ramub1lem1  15649  xpscfv  16138  xpsfrnel  16139  gexlem2  17913  frgpuptinv  18100  frgpup3lem  18106  gsummpt1n0  18280  dprdfid  18332  dpjrid  18377  abvtrivd  18756  mplsubrg  19354  znf1o  19814  znhash  19821  znunithash  19827  mamulid  20161  mamurid  20162  dmatid  20215  dmatmulcl  20220  scmatdmat  20235  mdetdiagid  20320  chpdmatlem2  20558  chpscmat  20561  chpidmat  20566  xkoccn  21327  iccpnfhmeo  22647  xrhmeo  22648  ioorinv2  23244  mbfi1fseqlem4  23386  ellimc2  23542  dvcobr  23610  ply1remlem  23821  dvtaylp  24023  0cxp  24307  lgsval3  24935  lgsdinn0  24965  dchrisumlem1  25073  dchrvmasumiflem1  25085  rpvmasum2  25096  dchrvmasumlem  25107  padicabv  25214  indispconn  30916  fnejoin1  31997  ptrecube  33027  poimirlem16  33043  poimirlem17  33044  poimirlem19  33046  poimirlem20  33047  fdc  33159  cdlemk40f  35673  sdrgacs  37238  blenn0  41633
  Copyright terms: Public domain W3C validator