Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mp3an13 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
Ref | Expression |
---|---|
mp3an13.1 | |
mp3an13.2 | |
mp3an13.3 |
Ref | Expression |
---|---|
mp3an13 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an13.1 | . 2 | |
2 | mp3an13.2 | . . 3 | |
3 | mp3an13.3 | . . 3 | |
4 | 2, 3 | mp3an3 1304 | . 2 |
5 | 1, 4 | mpan 420 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 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: pitonnlem1p1 7647 mulid1 7756 addltmul 8949 eluzaddi 9345 fz01en 9826 fznatpl1 9849 expubnd 10343 bernneq 10405 bernneq2 10406 efi4p 11413 efival 11428 cos2tsin 11447 cos01bnd 11454 cos01gt0 11458 dvds0 11497 odd2np1 11559 opoe 11581 gcdid 11663 blssioo 12703 tgioo 12704 rerestcntop 12708 sinperlem 12878 sincosq1sgn 12896 sincosq2sgn 12897 sinq12gt0 12900 cosq14gt0 12902 |
Copyright terms: Public domain | W3C validator |