![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iftruei | Structured version Visualization version Unicode version |
Description: Inference associated with iftrue 3878. (Contributed by BJ, 7-Oct-2018.) |
Ref | Expression |
---|---|
iftruei.1 |
![]() ![]() |
Ref | Expression |
---|---|
iftruei |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iftruei.1 |
. 2
![]() ![]() | |
2 | iftrue 3878 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-if 3873 |
This theorem is referenced by: oe0m 7238 ttukeylem4 8960 xnegpnf 11525 xnegmnf 11526 xaddpnf1 11542 xaddpnf2 11543 xaddmnf1 11544 xaddmnf2 11545 pnfaddmnf 11546 mnfaddpnf 11547 xmul01 11578 exp0 12314 swrd00 12828 sgn0 13229 lcm0val 14637 prmo2 15077 prmo3 15078 prmo5 15178 mulg0 16841 mvrid 18724 zzngim 19200 obsipid 19362 mamulid 19543 mamurid 19544 mat1dimid 19576 scmatf1 19633 mdetdiagid 19702 chpdmatlem3 19941 chpidmat 19948 fclscmpi 21122 ioorinv 22607 ioorinvOLD 22612 ig1pval2 23204 ig1pval2OLD 23210 dgrcolem2 23307 plydivlem4 23328 vieta1lem2 23343 0cxp 23690 cxpexp 23692 lgs0 24316 lgs2 24320 axlowdim 25070 gx0 26070 madjusmdetlem1 28727 signsw0glem 29514 rdgprc0 30511 bj-pr11val 31669 bj-pr22val 31683 mapdhval0 35364 hdmap1val0 35439 refsum2cnlem1 37421 cncfiooicclem1 37868 fouriersw 38207 hspmbllem1 38566 vtxvalsnop 39294 iedgvalsnop 39295 1loopgrvd2 39725 eupth2 40151 blen0 40891 0dig1 40928 |
Copyright terms: Public domain | W3C validator |