![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpd3an23 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.) |
Ref | Expression |
---|---|
mpd3an23.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
mpd3an23.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
mpd3an23.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
mpd3an23 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | mpd3an23.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | mpd3an23.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | mpd3an23.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | syl3anc 1249 |
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: exp0 10558 bcpasc 10781 bccl 10782 pw2dvds 12201 qnumdencoprm 12228 qeqnumdivden 12229 grpinvid 13019 qus0 13191 ghmid 13205 mgpvalg 13294 mgpex 13296 opprex 13440 unitgrpid 13485 qusmul2 13860 psrbaglesuppg 13967 dvef 14665 |
Copyright terms: Public domain | W3C validator |