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 1167 | . 2 |
4 | 1, 3 | mpan 420 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 947 |
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 949 |
This theorem is referenced by: mp3an12 1290 mp3an1i 1293 mp3anl1 1294 mp3an 1300 mp3an2i 1305 mp3an3an 1306 tfrlem9 6184 rdgexgg 6243 oaexg 6312 omexg 6315 oeiexg 6317 oav2 6327 nnaordex 6391 mulidnq 7165 1idpru 7367 addgt0sr 7551 muladd11 7863 cnegex 7908 negsubdi 7986 renegcl 7991 mulneg1 8125 ltaddpos 8182 addge01 8202 rimul 8315 recclap 8407 recidap 8414 recidap2 8415 recdivap2 8453 divdiv23apzi 8493 ltmul12a 8586 lemul12a 8588 mulgt1 8589 ltmulgt11 8590 gt0div 8596 ge0div 8597 ltdiv23i 8652 8th4div3 8907 gtndiv 9114 nn0ind 9133 fnn0ind 9135 xrre2 9572 ioorebasg 9726 fzen 9791 elfz0ubfz0 9870 expubnd 10318 le2sq2 10336 bernneq 10380 expnbnd 10383 faclbnd6 10458 bccl 10481 hashfacen 10547 shftfval 10561 mulreap 10604 caucvgrelemrec 10719 binom1p 11222 efi4p 11351 sinadd 11370 cosadd 11371 cos2t 11384 cos2tsin 11385 absefib 11404 efieq1re 11405 demoivreALT 11407 odd2np1 11497 opoe 11519 omoe 11520 opeo 11521 omeo 11522 gcdadd 11600 gcdmultiple 11635 algcvgblem 11657 algcvga 11659 isprm3 11726 coprm 11749 bl2ioo 12638 ioo2blex 12640 sinperlem 12816 |
Copyright terms: Public domain | W3C validator |