ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ifnefalse GIF 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 (𝐴𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)

Proof of Theorem ifnefalse
StepHypRef Expression
1 df-ne 2348 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 iffalse 3542 . 2 𝐴 = 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)
31, 2sylbi 121 1 (𝐴𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷)
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  9828  rexneg  9829  xaddpnf1  9845  xaddpnf2  9846  xaddmnf1  9847  xaddmnf2  9848  mnfaddpnf  9850  rexadd  9851  fztpval  10082  pcval  12295  xpsfrnel  12762  lgsval3  14389  lgsdinn0  14419
  Copyright terms: Public domain W3C validator