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

Theorem ifnefalse 3707
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 3706 directly in this case. It happens, e.g., in oevn0 6718. (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 2569 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 iffalse 3706 . 2  |-  ( -.  A  =  B  ->  if ( A  =  B ,  C ,  D
)  =  D )
31, 2sylbi 188 1  |-  ( A  =/=  B  ->  if ( A  =  B ,  C ,  D )  =  D )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2567   ifcif 3699
This theorem is referenced by:  xpima2  5274  axcc2lem  8272  xnegmnf  10752  rexneg  10753  xaddpnf1  10768  xaddpnf2  10769  xaddmnf1  10770  xaddmnf2  10771  mnfaddpnf  10773  rexadd  10774  fztpval  11063  sadcp1  12922  smupp1  12947  pcval  13173  ramtcl  13333  ramub1lem1  13349  xpscfv  13742  xpsfrnel  13743  gexlem2  15171  frgpuptinv  15358  frgpup3lem  15364  dprdfid  15530  dpjrid  15575  abvtrivd  15883  mplsubrg  16458  znf1o  16787  znhash  16794  znunithash  16800  xkoccn  17604  iccpnfhmeo  18923  xrhmeo  18924  ioorinv2  19420  mbfi1fseqlem4  19563  ellimc2  19717  dvcobr  19785  ply1remlem  20038  dvtaylp  20239  0cxp  20510  lgsval3  21051  lgsdinn0  21077  dchrisumlem1  21136  dchrvmasumiflem1  21148  rpvmasum2  21159  dchrvmasumlem  21170  padicabv  21277  indispcon  24874  fnejoin1  26287  fdc  26339  sdrgacs  27377  cdlemk40f  31401
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-ne 2569  df-if 3700
  Copyright terms: Public domain W3C validator