Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpd3an3 | Unicode version |
Description: An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.) |
Ref | Expression |
---|---|
mpd3an3.2 | |
mpd3an3.3 |
Ref | Expression |
---|---|
mpd3an3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpd3an3.2 | . 2 | |
2 | mpd3an3.3 | . . 3 | |
3 | 2 | 3expa 1185 | . 2 |
4 | 1, 3 | mpdan 418 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 963 |
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 965 |
This theorem is referenced by: stoic2b 1410 elovmpo 6021 oav 6401 omv 6402 oeiv 6403 f1oeng 6702 mulpipq2 7291 ltrnqg 7340 genipv 7429 subval 8067 subap0 8518 xaddval 9749 fzrevral3 10009 fzoval 10047 subsq2 10526 bcval 10623 dvdsmul1 11709 dvdsmul2 11710 gcdval 11843 eucalgval2 11930 setsvalg 12231 restval 12368 restin 12587 hmeofvalg 12714 cncfval 12970 rpcxpef 13226 rpcxpneg 13239 |
Copyright terms: Public domain | W3C validator |