| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > iftruei | Structured version Visualization version GIF version | ||
| Description: Inference associated with iftrue 4531. (Contributed by BJ, 7-Oct-2018.) |
| Ref | Expression |
|---|---|
| iftruei.1 | ⊢ 𝜑 |
| Ref | Expression |
|---|---|
| iftruei | ⊢ if(𝜑, 𝐴, 𝐵) = 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iftruei.1 | . 2 ⊢ 𝜑 | |
| 2 | iftrue 4531 | . 2 ⊢ (𝜑 → if(𝜑, 𝐴, 𝐵) = 𝐴) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ if(𝜑, 𝐴, 𝐵) = 𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 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-if 4526 |
| This theorem is referenced by: oe0m 8556 ttrcltr 9756 ttukeylem4 10552 xnegpnf 13251 xnegmnf 13252 xaddpnf1 13268 xaddpnf2 13269 xaddmnf1 13270 xaddmnf2 13271 pnfaddmnf 13272 mnfaddpnf 13273 xmul01 13309 exp0 14106 swrd00 14682 sgn0 15128 lcm0val 16631 prmo2 17078 prmo3 17079 prmo5 17166 mulg0 19092 zzngim 21571 obsipid 21742 mvrid 22004 mamulid 22447 mamurid 22448 mat1dimid 22480 scmatf1 22537 mdetdiagid 22606 chpdmatlem3 22846 chpidmat 22853 fclscmpi 24037 ioorinv 25611 ig1pval2 26216 dgrcolem2 26314 plydivlem4 26338 vieta1lem2 26353 0cxp 26708 cxpexp 26710 lgs0 27354 lgs2 27358 2lgs2 27449 left1s 27933 exps0 28410 axlowdim 28976 1loopgrvd2 29521 eupth2 30258 ex-prmo 30478 madjusmdetlem1 33826 signsw0glem 34568 breprexp 34648 ex-sategoelel 35426 rdgprc0 35794 bj-pr11val 37006 bj-pr22val 37020 mapdhval0 41727 hdmap1val0 41801 refsum2cnlem1 45042 liminf10ex 45789 cncfiooicclem1 45908 fouriersw 46246 hspmbllem1 46641 blen0 48493 0dig1 48530 |
| Copyright terms: Public domain | W3C validator |