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 4476 directly in this case. It happens, e.g., in oevn0 8134. (Contributed by David A. Wheeler, 15-May-2015.) |
Ref | Expression |
---|---|
ifnefalse | ⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 3017 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | iffalse 4476 | . 2 ⊢ (¬ 𝐴 = 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) | |
3 | 1, 2 | sylbi 219 | 1 ⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1533 ≠ wne 3016 ifcif 4467 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1777 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-ne 3017 df-if 4468 |
This theorem is referenced by: xpima2 6036 axcc2lem 9852 xnegmnf 12597 rexneg 12598 xaddpnf1 12613 xaddpnf2 12614 xaddmnf1 12615 xaddmnf2 12616 mnfaddpnf 12618 rexadd 12619 fztpval 12963 sadcp1 15798 smupp1 15823 pcval 16175 ramtcl 16340 ramub1lem1 16356 xpsfrnel 16829 gexlem2 18701 frgpuptinv 18891 frgpup3lem 18897 gsummpt1n0 19079 dprdfid 19133 dpjrid 19178 sdrgacs 19574 abvtrivd 19605 mplsubrg 20214 znf1o 20692 znhash 20699 znunithash 20705 mamulid 21044 mamurid 21045 dmatid 21098 dmatmulcl 21103 scmatdmat 21118 mdetdiagid 21203 chpdmatlem2 21441 chpscmat 21444 chpidmat 21449 xkoccn 22221 iccpnfhmeo 23543 xrhmeo 23544 ioorinv2 24170 mbfi1fseqlem4 24313 ellimc2 24469 dvcobr 24537 ply1remlem 24750 dvtaylp 24952 0cxp 25243 lgsval3 25885 lgsdinn0 25915 dchrisumlem1 26059 dchrvmasumiflem1 26071 rpvmasum2 26082 dchrvmasumlem 26093 padicabv 26200 indispconn 32476 ex-sategoelel 32663 fnejoin1 33711 ptrecube 34886 poimirlem16 34902 poimirlem17 34903 poimirlem19 34905 poimirlem20 34906 fdc 35014 cdlemk40f 38049 blenn0 44626 |
Copyright terms: Public domain | W3C validator |