![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an12 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.) |
Ref | Expression |
---|---|
mp3an12.1 |
![]() ![]() |
mp3an12.2 |
![]() ![]() |
mp3an12.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mp3an12 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an12.2 |
. 2
![]() ![]() | |
2 | mp3an12.1 |
. . 3
![]() ![]() | |
3 | mp3an12.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mp3an1 1256 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpan 415 |
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: mp3an12i 1273 ceqsralv 2639 brelrn 4615 funpr 5002 ener 6348 ltaddnq 6729 ltadd1sr 7085 mul02 7628 ltapi 7871 div0ap 7927 divclapzi 7972 divcanap1zi 7973 divcanap2zi 7974 divrecapzi 7975 divcanap3zi 7976 divcanap4zi 7977 divassapzi 7987 divmulapzi 7988 divdirapzi 7989 redivclapzi 8003 ltm1 8061 mulgt1 8078 recgt1i 8113 recreclt 8115 ltmul1i 8135 ltdiv1i 8136 ltmuldivi 8137 ltmul2i 8138 lemul1i 8139 lemul2i 8140 cju 8175 nnge1 8199 nngt0 8201 nnrecgt0 8213 elnnnn0c 8470 elnnz1 8525 recnz 8591 eluzsubi 8797 ge0gtmnf 9036 m1expcl2 9665 1exp 9672 m1expeven 9690 expubnd 9700 iexpcyc 9746 expnbnd 9763 expnlbnd 9764 remim 9966 imval2 10000 cjdivapi 10041 absdivapzi 10259 zeo3 10493 evend2 10514 |
Copyright terms: Public domain | W3C validator |