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

Theorem ifnefalse 3884
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 3881 directly in this case. It happens, e.g., in oevn0 7235. (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 2643 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 iffalse 3881 . 2  |-  ( -.  A  =  B  ->  if ( A  =  B ,  C ,  D
)  =  D )
31, 2sylbi 200 1  |-  ( A  =/=  B  ->  if ( A  =  B ,  C ,  D )  =  D )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1452    =/= wne 2641   ifcif 3872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-ne 2643  df-if 3873
This theorem is referenced by:  xpima2  5287  axcc2lem  8884  xnegmnf  11526  rexneg  11527  xaddpnf1  11542  xaddpnf2  11543  xaddmnf1  11544  xaddmnf2  11545  mnfaddpnf  11547  rexadd  11548  fztpval  11883  sadcp1  14508  smupp1  14533  pcval  14873  ramtcl  15043  ramtclOLD  15044  ramub1lem1  15063  xpscfv  15546  xpsfrnel  15547  gexlem2  17311  gexlem2OLD  17314  frgpuptinv  17499  frgpup3lem  17505  gsummpt1n0  17675  dprdfid  17728  dpjrid  17773  abvtrivd  18146  mplsubrg  18741  znf1o  19199  znhash  19206  znunithash  19212  mamulid  19543  mamurid  19544  dmatid  19597  dmatmulcl  19602  scmatdmat  19617  mdetdiagid  19702  chpdmatlem2  19940  chpscmat  19943  chpidmat  19948  xkoccn  20711  iccpnfhmeo  22051  xrhmeo  22052  ioorinv2  22606  ioorinv2OLD  22611  mbfi1fseqlem4  22755  ellimc2  22911  dvcobr  22979  ply1remlem  23192  dvtaylp  23404  0cxp  23690  lgsval3  24321  lgsdinn0  24347  dchrisumlem1  24406  dchrvmasumiflem1  24418  rpvmasum2  24429  dchrvmasumlem  24440  padicabv  24547  indispcon  30029  fnejoin1  31095  ptrecube  32004  poimirlem16  32020  poimirlem17  32021  poimirlem19  32023  poimirlem20  32024  fdc  32138  cdlemk40f  34557  sdrgacs  36138  blenn0  40892
  Copyright terms: Public domain W3C validator