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

Theorem ifnefalse 3749
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 3748 directly in this case. It happens, e.g., in oevn0 6762. (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 2603 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 iffalse 3748 . 2  |-  ( -.  A  =  B  ->  if ( A  =  B ,  C ,  D
)  =  D )
31, 2sylbi 189 1  |-  ( A  =/=  B  ->  if ( A  =  B ,  C ,  D )  =  D )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    =/= wne 2601   ifcif 3741
This theorem is referenced by:  xpima2  5318  axcc2lem  8321  xnegmnf  10801  rexneg  10802  xaddpnf1  10817  xaddpnf2  10818  xaddmnf1  10819  xaddmnf2  10820  mnfaddpnf  10822  rexadd  10823  fztpval  11112  sadcp1  12972  smupp1  12997  pcval  13223  ramtcl  13383  ramub1lem1  13399  xpscfv  13792  xpsfrnel  13793  gexlem2  15221  frgpuptinv  15408  frgpup3lem  15414  dprdfid  15580  dpjrid  15625  abvtrivd  15933  mplsubrg  16508  znf1o  16837  znhash  16844  znunithash  16850  xkoccn  17656  iccpnfhmeo  18975  xrhmeo  18976  ioorinv2  19472  mbfi1fseqlem4  19613  ellimc2  19769  dvcobr  19837  ply1remlem  20090  dvtaylp  20291  0cxp  20562  lgsval3  21103  lgsdinn0  21129  dchrisumlem1  21188  dchrvmasumiflem1  21200  rpvmasum2  21211  dchrvmasumlem  21222  padicabv  21329  indispcon  24926  fnejoin1  26411  fdc  26463  sdrgacs  27500  cdlemk40f  31790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-ne 2603  df-if 3742
  Copyright terms: Public domain W3C validator