![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an1 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.) |
Ref | Expression |
---|---|
mp3an1.1 |
![]() ![]() |
mp3an1.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mp3an1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an1.1 |
. 2
![]() ![]() | |
2 | mp3an1.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | 3expb 1204 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpan 424 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: mp3an12 1327 mp3an1i 1330 mp3anl1 1331 mp3an 1337 mp3an2i 1342 mp3an3an 1343 tfrlem9 6319 rdgexgg 6378 oaexg 6448 omexg 6451 oeiexg 6453 oav2 6463 nnaordex 6528 mulidnq 7387 1idpru 7589 addgt0sr 7773 muladd11 8088 cnegex 8133 negsubdi 8211 renegcl 8216 mulneg1 8350 ltaddpos 8407 addge01 8427 rimul 8540 recclap 8634 recidap 8641 recidap2 8642 recdivap2 8680 divdiv23apzi 8720 ltmul12a 8815 lemul12a 8817 mulgt1 8818 ltmulgt11 8819 gt0div 8825 ge0div 8826 ltdiv23i 8881 8th4div3 9136 gtndiv 9346 nn0ind 9365 fnn0ind 9367 xrre2 9819 ioorebasg 9973 fzen 10040 elfz0ubfz0 10122 expubnd 10574 le2sq2 10592 bernneq 10637 expnbnd 10640 faclbnd6 10719 bccl 10742 hashfacen 10811 shftfval 10825 mulreap 10868 caucvgrelemrec 10983 binom1p 11488 efi4p 11720 sinadd 11739 cosadd 11740 cos2t 11753 cos2tsin 11754 absefib 11773 efieq1re 11774 demoivreALT 11776 odd2np1 11872 opoe 11894 omoe 11895 opeo 11896 omeo 11897 gcdadd 11980 gcdmultiple 12015 algcvgblem 12043 algcvga 12045 isprm3 12112 coprm 12138 1arith2 12360 cnfldneg 13398 cnfldmulg 13401 cnfldexp 13402 zringmulg 13419 zringsubgval 13426 bl2ioo 13973 ioo2blex 13975 sinperlem 14160 logge0 14232 lgsdir2 14365 1lgs 14375 |
Copyright terms: Public domain | W3C validator |