![]() |
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 1326 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpan 424 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: pitonnlem1p1 7833 mulid1 7942 addltmul 9141 eluzaddi 9540 fz01en 10036 fznatpl1 10059 expubnd 10560 bernneq 10623 bernneq2 10624 efi4p 11706 efival 11721 cos2tsin 11740 cos01bnd 11747 cos01gt0 11751 dvds0 11794 odd2np1 11858 opoe 11880 gcdid 11967 pythagtriplem4 12248 blssioo 13705 tgioo 13706 rerestcntop 13710 sinperlem 13889 sincosq1sgn 13907 sincosq2sgn 13908 sinq12gt0 13911 cosq14gt0 13913 |
Copyright terms: Public domain | W3C validator |