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 1198 | . 2 |
4 | 1, 3 | mpdan 419 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 973 |
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 975 |
This theorem is referenced by: stoic2b 1423 elovmpo 6050 oav 6433 omv 6434 oeiv 6435 f1oeng 6735 mulpipq2 7333 ltrnqg 7382 genipv 7471 subval 8111 subap0 8562 xaddval 9802 fzrevral3 10063 fzoval 10104 subsq2 10583 bcval 10683 dvdsmul1 11775 dvdsmul2 11776 gcdval 11914 eucalgval2 12007 setsvalg 12446 restval 12585 ismhm 12685 restin 12970 hmeofvalg 13097 cncfval 13353 rpcxpef 13609 rpcxpneg 13622 lgsval 13699 |
Copyright terms: Public domain | W3C validator |