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 1186 | . 2 |
4 | 1, 3 | mpan 421 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 963 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 965 |
This theorem is referenced by: mp3an12 1309 mp3an1i 1312 mp3anl1 1313 mp3an 1319 mp3an2i 1324 mp3an3an 1325 tfrlem9 6266 rdgexgg 6325 oaexg 6395 omexg 6398 oeiexg 6400 oav2 6410 nnaordex 6474 mulidnq 7309 1idpru 7511 addgt0sr 7695 muladd11 8008 cnegex 8053 negsubdi 8131 renegcl 8136 mulneg1 8270 ltaddpos 8327 addge01 8347 rimul 8460 recclap 8552 recidap 8559 recidap2 8560 recdivap2 8598 divdiv23apzi 8638 ltmul12a 8731 lemul12a 8733 mulgt1 8734 ltmulgt11 8735 gt0div 8741 ge0div 8742 ltdiv23i 8797 8th4div3 9052 gtndiv 9259 nn0ind 9278 fnn0ind 9280 xrre2 9725 ioorebasg 9879 fzen 9945 elfz0ubfz0 10024 expubnd 10476 le2sq2 10494 bernneq 10538 expnbnd 10541 faclbnd6 10618 bccl 10641 hashfacen 10707 shftfval 10721 mulreap 10764 caucvgrelemrec 10879 binom1p 11382 efi4p 11614 sinadd 11633 cosadd 11634 cos2t 11647 cos2tsin 11648 absefib 11667 efieq1re 11668 demoivreALT 11670 odd2np1 11763 opoe 11785 omoe 11786 opeo 11787 omeo 11788 gcdadd 11868 gcdmultiple 11903 algcvgblem 11925 algcvga 11927 isprm3 11994 coprm 12018 bl2ioo 12942 ioo2blex 12944 sinperlem 13129 logge0 13201 |
Copyright terms: Public domain | W3C validator |