| 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 4534 directly in this case. It happens, e.g., in oevn0 8553. (Contributed by David A. Wheeler, 15-May-2015.) |
| Ref | Expression |
|---|---|
| ifnefalse | ⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ne 2941 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
| 2 | iffalse 4534 | . 2 ⊢ (¬ 𝐴 = 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) | |
| 3 | 1, 2 | sylbi 217 | 1 ⊢ (𝐴 ≠ 𝐵 → if(𝐴 = 𝐵, 𝐶, 𝐷) = 𝐷) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 = wceq 1540 ≠ wne 2940 ifcif 4525 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-if 4526 |
| This theorem is referenced by: xpima2 6204 axcc2lem 10476 xnegmnf 13252 rexneg 13253 xaddpnf1 13268 xaddpnf2 13269 xaddmnf1 13270 xaddmnf2 13271 mnfaddpnf 13273 rexadd 13274 fztpval 13626 sadcp1 16492 smupp1 16517 pcval 16882 ramtcl 17048 ramub1lem1 17064 xpsfrnel 17607 gexlem2 19600 frgpuptinv 19789 frgpup3lem 19795 gsummpt1n0 19983 dprdfid 20037 dpjrid 20082 sdrgacs 20802 abvtrivd 20833 znf1o 21570 znhash 21577 znunithash 21583 mplsubrg 22025 psdmul 22170 mamulid 22447 mamurid 22448 dmatid 22501 dmatmulcl 22506 scmatdmat 22521 mdetdiagid 22606 chpdmatlem2 22845 chpscmat 22848 chpidmat 22853 xkoccn 23627 iccpnfhmeo 24976 xrhmeo 24977 ioorinv2 25610 mbfi1fseqlem4 25753 ellimc2 25912 dvcobr 25983 dvcobrOLD 25984 ply1remlem 26204 dvtaylp 26412 0cxp 26708 lgsval3 27359 lgsdinn0 27389 dchrisumlem1 27533 dchrvmasumiflem1 27545 rpvmasum2 27556 dchrvmasumlem 27567 padicabv 27674 indispconn 35239 ex-sategoelel 35426 fnejoin1 36369 ptrecube 37627 poimirlem16 37643 poimirlem17 37644 poimirlem19 37646 poimirlem20 37647 fdc 37752 cdlemk40f 40921 fiabv 42546 blenn0 48494 |
| Copyright terms: Public domain | W3C validator |