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

Theorem ifnefalse 3649
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 3648 directly in this case. It happens, e.g., in oevn0 6601. (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 2523 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 iffalse 3648 . 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 1642    =/= wne 2521   ifcif 3641
This theorem is referenced by:  axcc2lem  8152  xnegmnf  10629  rexneg  10630  xaddpnf1  10645  xaddpnf2  10646  xaddmnf1  10647  xaddmnf2  10648  mnfaddpnf  10650  rexadd  10651  fztpval  10937  sadcp1  12743  smupp1  12768  pcval  12994  ramtcl  13154  ramub1lem1  13170  xpscfv  13563  xpsfrnel  13564  gexlem2  14992  frgpuptinv  15179  frgpup3lem  15185  dprdfid  15351  dpjrid  15396  abvtrivd  15704  mplsubrg  16283  znf1o  16611  znhash  16618  znunithash  16624  xkoccn  17419  iccpnfhmeo  18547  xrhmeo  18548  ioorinv2  19034  mbfi1fseqlem4  19177  ellimc2  19331  dvcobr  19399  ply1remlem  19652  dvtaylp  19853  0cxp  20124  lgsval3  20665  lgsdinn0  20691  dchrisumlem1  20750  dchrvmasumiflem1  20762  rpvmasum2  20773  dchrvmasumlem  20784  padicabv  20891  indispcon  24169  itg2addnclem  25492  itg2addnc  25494  fnejoin1  25641  fdc  25779  sdrgacs  26832  cdlemk40f  31177
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-ne 2523  df-if 3642
  Copyright terms: Public domain W3C validator