![]() |
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 4499 directly in this case. It happens, e.g., in oevn0 8465. (Contributed by David A. Wheeler, 15-May-2015.) |
Ref | Expression |
---|---|
ifnefalse | ⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2941 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | iffalse 4499 | . 2 ⊢ (¬ 𝐴 = 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) | |
3 | 1, 2 | sylbi 216 | 1 ⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1542 ≠ wne 2940 ifcif 4490 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2941 df-if 4491 |
This theorem is referenced by: xpima2 6140 axcc2lem 10380 xnegmnf 13138 rexneg 13139 xaddpnf1 13154 xaddpnf2 13155 xaddmnf1 13156 xaddmnf2 13157 mnfaddpnf 13159 rexadd 13160 fztpval 13512 sadcp1 16343 smupp1 16368 pcval 16724 ramtcl 16890 ramub1lem1 16906 xpsfrnel 17452 gexlem2 19372 frgpuptinv 19561 frgpup3lem 19567 gsummpt1n0 19750 dprdfid 19804 dpjrid 19849 sdrgacs 20311 abvtrivd 20342 znf1o 20981 znhash 20988 znunithash 20994 mplsubrg 21434 mamulid 21813 mamurid 21814 dmatid 21867 dmatmulcl 21872 scmatdmat 21887 mdetdiagid 21972 chpdmatlem2 22211 chpscmat 22214 chpidmat 22219 xkoccn 22993 iccpnfhmeo 24331 xrhmeo 24332 ioorinv2 24962 mbfi1fseqlem4 25106 ellimc2 25264 dvcobr 25333 ply1remlem 25550 dvtaylp 25752 0cxp 26044 lgsval3 26686 lgsdinn0 26716 dchrisumlem1 26860 dchrvmasumiflem1 26872 rpvmasum2 26883 dchrvmasumlem 26894 padicabv 27001 indispconn 33892 ex-sategoelel 34079 fnejoin1 34893 ptrecube 36128 poimirlem16 36144 poimirlem17 36145 poimirlem19 36147 poimirlem20 36148 fdc 36254 cdlemk40f 39432 blenn0 46749 |
Copyright terms: Public domain | W3C validator |