ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ifnefalse Unicode version

Theorem ifnefalse 3545
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 versus applying iffalse 3542 directly in this case. (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 2348 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 iffalse 3542 . 2  |-  ( -.  A  =  B  ->  if ( A  =  B ,  C ,  D
)  =  D )
31, 2sylbi 121 1  |-  ( A  =/=  B  ->  if ( A  =  B ,  C ,  D )  =  D )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1353    =/= wne 2347   ifcif 3534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-ne 2348  df-if 3535
This theorem is referenced by:  xnegmnf  9827  rexneg  9828  xaddpnf1  9844  xaddpnf2  9845  xaddmnf1  9846  xaddmnf2  9847  mnfaddpnf  9849  rexadd  9850  fztpval  10080  pcval  12290  lgsval3  14312  lgsdinn0  14342
  Copyright terms: Public domain W3C validator