![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mp3an3 | Structured version Visualization version Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Ref | Expression |
---|---|
mp3an3.1 |
![]() ![]() |
mp3an3.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mp3an3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an3.1 |
. 2
![]() ![]() | |
2 | mp3an3.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | 3expia 1217 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpi 20 |
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 |
This theorem depends on definitions: df-bi 190 df-an 377 df-3an 993 |
This theorem is referenced by: mp3an13 1364 mp3an23 1365 mp3anl3 1369 opelxp 4886 ov 6448 ovmpt2a 6459 ovmpt2 6464 oaword1 7284 oneo 7313 oeoalem 7328 oeoelem 7330 nnaword1 7361 nnneo 7383 erov 7491 enrefg 7632 f1imaen 7662 mapxpen 7769 acnlem 8510 cdacomen 8642 infmap 9032 canthnumlem 9104 tskin 9215 tsksn 9216 tsk0 9219 gruxp 9263 gruina 9274 genpprecl 9457 addsrpr 9530 mulsrpr 9531 supsrlem 9566 mulid1 9671 00id 9839 mul02lem1 9840 ltneg 10147 leneg 10150 suble0 10161 div1 10332 nnaddcl 10664 nnmulcl 10665 nnge1 10668 nnsub 10681 2halves 10875 halfaddsub 10880 addltmul 10882 zleltp1 11021 nnaddm1cl 11027 zextlt 11044 eluzp1p1 11218 uzaddcl 11249 znq 11302 xrre 11498 xrre2 11499 fzshftral 11917 fraclt1 12076 expadd 12352 expmul 12355 expubnd 12371 sqmul 12376 bernneq 12436 faclbnd2 12514 faclbnd6 12522 hashgadd 12594 hashun2 12600 hashssdif 12627 hashfun 12648 ccatlcan 12871 ccatrcan 12872 shftval3 13194 sqrlem1 13361 caubnd2 13475 bpoly2 14165 bpoly3 14166 fsumcube 14168 efexp 14210 efival 14261 cos01gt0 14300 odd2np1 14420 divalglem5OLD 14431 divalglem5 14432 gcdmultiple 14573 sqgcd 14581 nn0seqcvgd 14584 phiprmpw 14779 eulerthlem2 14785 odzcllem 14792 odzcllemOLD 14798 omoe 14817 opeo 14818 pythagtriplem15 14834 pythagtriplem17 14836 pcelnn 14874 4sqlem3 14949 xpscfn 15520 fullfunc 15866 fthfunc 15867 prfcl 16143 curf1cl 16168 curfcl 16172 hofcl 16199 odinv 17267 lsmelvalix 17348 dprdval 17690 lsp0 18287 lss0v 18294 coe1scl 18935 zndvds0 19176 frlmlbs 19410 lindfres 19436 lmisfree 19455 ntrin 20131 lpsscls 20212 restperf 20255 txuni2 20635 txopn 20672 elqtop2 20771 xkocnv 20884 ptcmp 21128 xblpnfps 21465 xblpnf 21466 bl2in 21470 unirnblps 21489 unirnbl 21490 blpnfctr 21506 dscopn 21643 bcthlem4 22350 minveclem2 22423 minveclem4 22429 minveclem2OLD 22435 minveclem4OLD 22441 icombl 22573 i1fadd 22709 i1fmul 22710 dvn1 22936 dvexp3 22986 plyconst 23216 plyid 23219 sincosq1eq 23523 sinord 23539 cxpp1 23681 cxpsqrtlem 23703 cxpsqrt 23704 angneg 23788 dcubic 23828 issqf 24119 ppiub 24188 bposlem1 24268 bposlem2 24269 bposlem9 24276 axlowdimlem6 25033 axlowdimlem14 25041 axcontlem2 25051 wwlkn0s 25489 clwwlkn2 25559 rusgranumwlkb0 25737 gx0 26045 gx1 26046 gxm1 26052 gxnn0add 26058 gxnn0mul 26061 ipasslem1 26528 ipasslem2 26529 ipasslem11 26537 minvecolem2 26573 minvecolem3 26574 minvecolem4 26578 minvecolem2OLD 26583 minvecolem3OLD 26584 minvecolem4OLD 26588 shsva 27029 h1datomi 27290 lnfnmuli 27753 leopsq 27838 nmopleid 27848 opsqrlem6 27854 pjnmopi 27857 hstle 27939 csmdsymi 28043 atcvatlem 28094 elsx 29067 dya2iocnrect 29153 cvmliftphtlem 30090 wlimeq12 30552 nofulllem4 30644 fvray 30958 fvline 30961 tailfb 31083 tan2h 31983 poimirlem32 32018 mblfinlem4 32026 mbfresfi 32033 mbfposadd 32034 dvtanlemOLD 32037 itg2addnc 32042 ftc1anclem5 32067 ftc1anclem8 32070 dvasin 32074 heiborlem7 32195 igenidl 32342 atlatmstc 32931 dihglblem2N 34908 eldioph4b 35700 diophren 35702 rmxp1 35826 rmyp1 35827 rmxm1 35828 rmym1 35829 wepwso 35947 pfx2 39090 structgrssvtxlem 39267 pthdlem2 39890 0ewlk 39924 dig0 40786 onetansqsecsq 40850 cotsqcscsq 40851 dpfrac1 40861 |
Copyright terms: Public domain | W3C validator |