![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ifnefalse | Structured version Visualization version GIF version |
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 4285 directly in this case. It happens, e.g., in oevn0 7834. (Contributed by David A. Wheeler, 15-May-2015.) |
Ref | Expression |
---|---|
ifnefalse | ⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2971 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | iffalse 4285 | . 2 ⊢ (¬ 𝐴 = 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) | |
3 | 1, 2 | sylbi 209 | 1 ⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1653 ≠ wne 2970 ifcif 4276 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-ext 2776 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-clab 2785 df-cleq 2791 df-clel 2794 df-ne 2971 df-if 4277 |
This theorem is referenced by: xpima2 5794 axcc2lem 9545 xnegmnf 12287 rexneg 12288 xaddpnf1 12303 xaddpnf2 12304 xaddmnf1 12305 xaddmnf2 12306 mnfaddpnf 12308 rexadd 12309 fztpval 12653 sadcp1 15509 smupp1 15534 pcval 15879 ramtcl 16044 ramub1lem1 16060 xpscfv 16534 xpsfrnel 16535 gexlem2 18307 frgpuptinv 18496 frgpup3lem 18502 gsummpt1n0 18676 dprdfid 18729 dpjrid 18774 abvtrivd 19155 mplsubrg 19760 znf1o 20218 znhash 20225 znunithash 20231 mamulid 20569 mamurid 20570 dmatid 20624 dmatmulcl 20629 scmatdmat 20644 mdetdiagid 20729 chpdmatlem2 20969 chpscmat 20972 chpidmat 20977 xkoccn 21748 iccpnfhmeo 23069 xrhmeo 23070 ioorinv2 23680 mbfi1fseqlem4 23823 ellimc2 23979 dvcobr 24047 ply1remlem 24260 dvtaylp 24462 0cxp 24750 lgsval3 25389 lgsdinn0 25419 dchrisumlem1 25527 dchrvmasumiflem1 25539 rpvmasum2 25550 dchrvmasumlem 25561 padicabv 25668 indispconn 31726 fnejoin1 32868 ptrecube 33891 poimirlem16 33907 poimirlem17 33908 poimirlem19 33910 poimirlem20 33911 fdc 34021 cdlemk40f 36933 sdrgacs 38545 blenn0 43155 |
Copyright terms: Public domain | W3C validator |