![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iffalsei | Structured version Visualization version GIF version |
Description: Inference associated with iffalse 4533. (Contributed by BJ, 7-Oct-2018.) |
Ref | Expression |
---|---|
iffalsei.1 | ⊢ ¬ 𝜑 |
Ref | Expression |
---|---|
iffalsei | ⊢ if(𝜑, 𝐴, 𝐵) = 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iffalsei.1 | . 2 ⊢ ¬ 𝜑 | |
2 | iffalse 4533 | . 2 ⊢ (¬ 𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐵) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ if(𝜑, 𝐴, 𝐵) = 𝐵 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1542 ifcif 4524 |
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-if 4525 |
This theorem is referenced by: ssttrcl 9697 ttrclselem2 9708 sum0 15654 prod0 15874 prmo4 17048 prmo6 17050 itg0 25266 vieta1lem2 25793 right1s 27357 vtxval0 28266 iedgval0 28267 ex-prmo 29679 dfrdg2 34698 dfrdg4 34854 fwddifnp1 35068 bj-pr21val 35799 bj-pr22val 35805 imsqrtvalex 42268 clsk1indlem4 42666 clsk1indlem1 42667 refsum2cnlem1 43592 limsup10ex 44362 iblempty 44554 fouriersw 44820 |
Copyright terms: Public domain | W3C validator |