![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpg | GIF version |
Description: Modus ponens combined with generalization. (Contributed by NM, 24-May-1994.) |
Ref | Expression |
---|---|
mpg.1 | ⊢ (∀𝑥𝜑 → 𝜓) |
mpg.2 | ⊢ 𝜑 |
Ref | Expression |
---|---|
mpg | ⊢ 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpg.2 | . . 3 ⊢ 𝜑 | |
2 | 1 | ax-gen 1460 | . 2 ⊢ ∀𝑥𝜑 |
3 | mpg.1 | . 2 ⊢ (∀𝑥𝜑 → 𝜓) | |
4 | 2, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1362 |
This theorem was proved from axioms: ax-mp 5 ax-gen 1460 |
This theorem is referenced by: alimi 1466 albii 1481 a5i 1554 nfal 1587 eximi 1611 exbii 1616 19.9h 1654 hbn 1665 chvarfv 1711 chvar 1768 equsb1 1796 equsb2 1797 chvarvv 1920 chvarv 1949 moimi 2103 2eumo 2126 vtoclf 2805 vtocl2 2807 vtocl3 2808 spcimgf 2832 spcimegf 2833 spcgf 2834 spcegf 2835 mosub 2930 csbexa 4147 nalset 4148 ssopab2i 4295 pwnex 4467 eusv2nf 4474 iotabii 5219 fvmptss2 5611 eufnfv 5767 riotaexg 5855 xpcomco 6851 bj-ex 14967 ch2var 14972 bj-vtoclgf 14981 elabgf1 14984 bj-rspg 14992 sumdc2 15004 bdsepnf 15093 bj-nalset 15100 setindf 15171 strcollnf 15190 |
Copyright terms: Public domain | W3C validator |