![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 14-May-1999.) |
Ref | Expression |
---|---|
mp3an.1 |
![]() ![]() |
mp3an.2 |
![]() ![]() |
mp3an.3 |
![]() ![]() |
mp3an.4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mp3an |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an.2 |
. 2
![]() ![]() | |
2 | mp3an.3 |
. 2
![]() ![]() | |
3 | mp3an.1 |
. . 3
![]() ![]() | |
4 | mp3an.4 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | mp3an1 1256 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 2, 5 | mp2an 417 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 df-3an 922 |
This theorem is referenced by: vtocl3 2664 raltp 3468 rextp 3469 ordtriexmidlem 4292 ordtri2or2exmidlem 4298 onsucelsucexmidlem 4301 ordsoexmid 4334 funopg 4985 ftp 5401 caovass 5713 caovdi 5732 ofmres 5815 mpt2fvexi 5884 dmtpos 5926 rntpos 5927 dftpos3 5932 tpostpos 5934 xpcomen 6393 unfiexmid 6463 1lt2pi 6628 1lt2nq 6694 halfnqq 6698 m1p1sr 7035 m1m1sr 7036 addassi 7225 mulassi 7226 adddii 7227 adddiri 7228 lttri 7318 lelttri 7319 ltletri 7320 letri 7321 mul12i 7357 mul32i 7358 add12i 7374 add32i 7375 addcani 7393 addcan2i 7394 subaddi 7498 subadd2i 7499 subsub23i 7501 addsubassi 7502 addsubi 7503 subcani 7504 subcan2i 7505 pnncani 7506 subdii 7614 subdiri 7615 ltadd2i 7627 ltadd1i 7706 leadd1i 7707 leadd2i 7708 ltsubaddi 7709 lesubaddi 7710 ltsubadd2i 7711 lesubadd2i 7712 ltaddsubi 7713 gtapii 7835 mulcanapi 7860 divclapi 7945 divcanap2i 7946 divcanap1i 7947 divrecapi 7948 divcanap3i 7949 divcanap4i 7950 divassapi 7959 divdirapi 7960 div23api 7961 div11api 7962 1mhlfehlf 8352 halfpm6th 8354 3halfnz 8561 unirnioo 9108 nnenom 9552 m1expcl2 9631 i4 9710 expnass 9713 bcn1 9818 hashinfom 9838 abs3difi 10227 3dvdsdec 10456 3dvds2dec 10457 ndvdsi 10524 flodddiv4 10525 3lcm2e6woprm 10659 6lcm4e12 10660 3prm 10701 znnen 10802 ex-fl 10807 |
Copyright terms: Public domain | W3C validator |