![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ifnefalse | Structured version Visualization version Unicode 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 vs. applying iffalse 3890 directly in this case. It happens, e.g., in oevn0 7217. (Contributed by David A. Wheeler, 15-May-2015.) |
Ref | Expression |
---|---|
ifnefalse |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2624 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | iffalse 3890 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylbi 199 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-ne 2624 df-if 3882 |
This theorem is referenced by: xpima2 5281 axcc2lem 8866 xnegmnf 11503 rexneg 11504 xaddpnf1 11519 xaddpnf2 11520 xaddmnf1 11521 xaddmnf2 11522 mnfaddpnf 11524 rexadd 11525 fztpval 11857 sadcp1 14429 smupp1 14454 pcval 14794 ramtcl 14964 ramtclOLD 14965 ramub1lem1 14984 xpscfv 15468 xpsfrnel 15469 gexlem2 17233 gexlem2OLD 17236 frgpuptinv 17421 frgpup3lem 17427 gsummpt1n0 17597 dprdfid 17650 dpjrid 17695 abvtrivd 18068 mplsubrg 18664 znf1o 19122 znhash 19129 znunithash 19135 mamulid 19466 mamurid 19467 dmatid 19520 dmatmulcl 19525 scmatdmat 19540 mdetdiagid 19625 chpdmatlem2 19863 chpscmat 19866 chpidmat 19871 xkoccn 20634 iccpnfhmeo 21973 xrhmeo 21974 ioorinv2 22527 ioorinv2OLD 22532 mbfi1fseqlem4 22676 ellimc2 22832 dvcobr 22900 ply1remlem 23113 dvtaylp 23325 0cxp 23611 lgsval3 24242 lgsdinn0 24268 dchrisumlem1 24327 dchrvmasumiflem1 24339 rpvmasum2 24350 dchrvmasumlem 24361 padicabv 24468 indispcon 29957 fnejoin1 31024 ptrecube 31940 poimirlem16 31956 poimirlem17 31957 poimirlem19 31959 poimirlem20 31960 fdc 32074 cdlemk40f 34486 sdrgacs 36067 blenn0 40437 |
Copyright terms: Public domain | W3C validator |