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 1182 | . 2 |
4 | 1, 3 | mpan 420 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 962 |
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 964 |
This theorem is referenced by: mp3an12 1305 mp3an1i 1308 mp3anl1 1309 mp3an 1315 mp3an2i 1320 mp3an3an 1321 tfrlem9 6216 rdgexgg 6275 oaexg 6344 omexg 6347 oeiexg 6349 oav2 6359 nnaordex 6423 mulidnq 7197 1idpru 7399 addgt0sr 7583 muladd11 7895 cnegex 7940 negsubdi 8018 renegcl 8023 mulneg1 8157 ltaddpos 8214 addge01 8234 rimul 8347 recclap 8439 recidap 8446 recidap2 8447 recdivap2 8485 divdiv23apzi 8525 ltmul12a 8618 lemul12a 8620 mulgt1 8621 ltmulgt11 8622 gt0div 8628 ge0div 8629 ltdiv23i 8684 8th4div3 8939 gtndiv 9146 nn0ind 9165 fnn0ind 9167 xrre2 9604 ioorebasg 9758 fzen 9823 elfz0ubfz0 9902 expubnd 10350 le2sq2 10368 bernneq 10412 expnbnd 10415 faclbnd6 10490 bccl 10513 hashfacen 10579 shftfval 10593 mulreap 10636 caucvgrelemrec 10751 binom1p 11254 efi4p 11424 sinadd 11443 cosadd 11444 cos2t 11457 cos2tsin 11458 absefib 11477 efieq1re 11478 demoivreALT 11480 odd2np1 11570 opoe 11592 omoe 11593 opeo 11594 omeo 11595 gcdadd 11673 gcdmultiple 11708 algcvgblem 11730 algcvga 11732 isprm3 11799 coprm 11822 bl2ioo 12711 ioo2blex 12713 sinperlem 12889 |
Copyright terms: Public domain | W3C validator |