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 1166 | . 2 |
4 | 1, 3 | mpdan 417 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 947 |
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 949 |
This theorem is referenced by: stoic2b 1391 elovmpo 5939 oav 6318 omv 6319 oeiv 6320 f1oeng 6619 mulpipq2 7147 ltrnqg 7196 genipv 7285 subval 7922 subap0 8373 xaddval 9596 fzrevral3 9855 fzoval 9893 subsq2 10368 bcval 10463 dvdsmul1 11442 dvdsmul2 11443 gcdval 11575 eucalgval2 11661 setsvalg 11916 restval 12053 restin 12272 hmeofvalg 12399 cncfval 12655 |
Copyright terms: Public domain | W3C validator |