![]() |
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 1379 | . 2 ⊢ ∀𝑥𝜑 |
3 | mpg.1 | . 2 ⊢ (∀𝑥𝜑 → 𝜓) | |
4 | 2, 3 | ax-mp 7 | 1 ⊢ 𝜓 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1283 |
This theorem was proved from axioms: ax-mp 7 ax-gen 1379 |
This theorem is referenced by: alimi 1385 albii 1400 a5i 1476 eximi 1532 exbii 1537 19.9h 1575 hbn 1585 chvar 1682 equsb1 1710 equsb2 1711 chvarv 1855 moimi 2008 2eumo 2031 vtoclf 2661 vtocl2 2663 vtocl3 2664 spcimgf 2687 spcimegf 2688 spcgf 2689 spcegf 2690 mosub 2779 csbexa 3927 nalset 3928 ssopab2i 4060 eusv2nf 4234 iotabii 4939 fvmptss2 5299 eufnfv 5441 riotaexg 5523 xpcomco 6391 bj-ex 10833 ch2var 10838 bj-vtoclgf 10846 elabgf1 10849 bj-rspg 10857 sumdc2 10869 bdsepnf 10946 bj-nalset 10953 setindf 11028 strcollnf 11047 |
Copyright terms: Public domain | W3C validator |