![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mp3an23 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.) |
Ref | Expression |
---|---|
mp3an23.1 |
![]() ![]() |
mp3an23.2 |
![]() ![]() |
mp3an23.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mp3an23 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mp3an23.1 |
. 2
![]() ![]() | |
2 | mp3an23.2 |
. . 3
![]() ![]() | |
3 | mp3an23.3 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mp3an3 1337 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpan2 425 |
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 982 |
This theorem is referenced by: sbciegf 3009 ac6sfi 6930 dju0en 7248 1qec 7422 ltaddnq 7441 halfnqq 7444 1idsr 7802 pn0sr 7805 ltm1sr 7811 muleqadd 8660 halfcl 9180 rehalfcl 9181 half0 9182 2halves 9183 halfpos2 9184 halfnneg2 9186 halfaddsub 9188 nneoor 9390 zeo 9393 fztp 10114 modqfrac 10374 iexpcyc 10665 bcn2 10785 bcpasc 10787 imre 10901 reim 10902 crim 10908 addcj 10941 imval2 10944 sinf 11753 efi4p 11766 resin4p 11767 recos4p 11768 sinneg 11775 efival 11781 cosadd 11786 sinmul 11793 sinbnd 11801 cosbnd 11802 ef01bndlem 11805 sin01bnd 11806 cos01bnd 11807 sin01gt0 11810 cos01gt0 11811 sin02gt0 11812 odd2np1lem 11918 odd2np1 11919 pythagtriplem12 12318 pockthi 12401 opprsubrngg 13583 isridl 13844 zlmval 13948 zlmlemg 13949 zlmsca 13953 zlmvscag 13954 mopnex 14490 sincosq1lem 14731 sincosq2sgn 14733 sincosq3sgn 14734 sincosq4sgn 14735 sinq12gt0 14736 abssinper 14752 coskpi 14754 rpcxpsqrt 14827 logsqrt 14828 2lgsoddprmlem2 14940 |
Copyright terms: Public domain | W3C validator |