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

Theorem ifnefalse 3573
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 3572 directly in this case. It happens, e.g., in oevn0 6514. (Contributed by David A. Wheeler, 15-May-2015.)
Assertion
Ref Expression
ifnefalse  |-  ( A  =/=  B  ->  if ( A  =  B ,  C ,  D )  =  D )

Proof of Theorem ifnefalse
StepHypRef Expression
1 df-ne 2448 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 iffalse 3572 . 2  |-  ( -.  A  =  B  ->  if ( A  =  B ,  C ,  D
)  =  D )
31, 2sylbi 187 1  |-  ( A  =/=  B  ->  if ( A  =  B ,  C ,  D )  =  D )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    =/= wne 2446   ifcif 3565
This theorem is referenced by:  axcc2lem  8062  xnegmnf  10537  rexneg  10538  xaddpnf1  10553  xaddpnf2  10554  xaddmnf1  10555  xaddmnf2  10556  mnfaddpnf  10558  rexadd  10559  fztpval  10845  sadcp1  12646  smupp1  12671  pcval  12897  ramtcl  13057  ramub1lem1  13073  xpscfv  13464  xpsfrnel  13465  gexlem2  14893  frgpuptinv  15080  frgpup3lem  15086  dprdfid  15252  dpjrid  15297  abvtrivd  15605  mplsubrg  16184  znf1o  16505  znhash  16512  znunithash  16518  xkoccn  17313  iccpnfhmeo  18443  xrhmeo  18444  ioorinv2  18930  mbfi1fseqlem4  19073  ellimc2  19227  dvcobr  19295  ply1remlem  19548  dvtaylp  19749  0cxp  20013  lgsval3  20553  lgsdinn0  20579  dchrisumlem1  20638  dchrvmasumiflem1  20650  rpvmasum2  20661  dchrvmasumlem  20672  padicabv  20779  indispcon  23765  isconc3  26008  fnejoin1  26317  fdc  26455  sdrgacs  27509  cdlemk40f  31108
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-ne 2448  df-if 3566
  Copyright terms: Public domain W3C validator