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 1199 | . 2 |
4 | 1, 3 | mpan 422 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 973 |
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 975 |
This theorem is referenced by: mp3an12 1322 mp3an1i 1325 mp3anl1 1326 mp3an 1332 mp3an2i 1337 mp3an3an 1338 tfrlem9 6298 rdgexgg 6357 oaexg 6427 omexg 6430 oeiexg 6432 oav2 6442 nnaordex 6507 mulidnq 7351 1idpru 7553 addgt0sr 7737 muladd11 8052 cnegex 8097 negsubdi 8175 renegcl 8180 mulneg1 8314 ltaddpos 8371 addge01 8391 rimul 8504 recclap 8596 recidap 8603 recidap2 8604 recdivap2 8642 divdiv23apzi 8682 ltmul12a 8776 lemul12a 8778 mulgt1 8779 ltmulgt11 8780 gt0div 8786 ge0div 8787 ltdiv23i 8842 8th4div3 9097 gtndiv 9307 nn0ind 9326 fnn0ind 9328 xrre2 9778 ioorebasg 9932 fzen 9999 elfz0ubfz0 10081 expubnd 10533 le2sq2 10551 bernneq 10596 expnbnd 10599 faclbnd6 10678 bccl 10701 hashfacen 10771 shftfval 10785 mulreap 10828 caucvgrelemrec 10943 binom1p 11448 efi4p 11680 sinadd 11699 cosadd 11700 cos2t 11713 cos2tsin 11714 absefib 11733 efieq1re 11734 demoivreALT 11736 odd2np1 11832 opoe 11854 omoe 11855 opeo 11856 omeo 11857 gcdadd 11940 gcdmultiple 11975 algcvgblem 12003 algcvga 12005 isprm3 12072 coprm 12098 1arith2 12320 bl2ioo 13336 ioo2blex 13338 sinperlem 13523 logge0 13595 lgsdir2 13728 1lgs 13738 |
Copyright terms: Public domain | W3C validator |