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 1315 | . 2 |
5 | 1, 4 | mpan 421 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 967 |
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 969 |
This theorem is referenced by: pitonnlem1p1 7778 mulid1 7887 addltmul 9084 eluzaddi 9483 fz01en 9978 fznatpl1 10001 expubnd 10502 bernneq 10564 bernneq2 10565 efi4p 11644 efival 11659 cos2tsin 11678 cos01bnd 11685 cos01gt0 11689 dvds0 11732 odd2np1 11795 opoe 11817 gcdid 11904 pythagtriplem4 12179 blssioo 13092 tgioo 13093 rerestcntop 13097 sinperlem 13276 sincosq1sgn 13294 sincosq2sgn 13295 sinq12gt0 13298 cosq14gt0 13300 |
Copyright terms: Public domain | W3C validator |