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 1436 | . 2 ⊢ ∀𝑥𝜑 |
3 | mpg.1 | . 2 ⊢ (∀𝑥𝜑 → 𝜓) | |
4 | 2, 3 | ax-mp 5 | 1 ⊢ 𝜓 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1340 |
This theorem was proved from axioms: ax-mp 5 ax-gen 1436 |
This theorem is referenced by: alimi 1442 albii 1457 a5i 1530 nfal 1563 eximi 1587 exbii 1592 19.9h 1630 hbn 1641 chvarfv 1687 chvar 1744 equsb1 1772 equsb2 1773 chvarvv 1895 chvarv 1924 moimi 2078 2eumo 2101 vtoclf 2777 vtocl2 2779 vtocl3 2780 spcimgf 2804 spcimegf 2805 spcgf 2806 spcegf 2807 mosub 2902 csbexa 4108 nalset 4109 ssopab2i 4252 pwnex 4424 eusv2nf 4431 iotabii 5172 fvmptss2 5558 eufnfv 5712 riotaexg 5799 xpcomco 6786 bj-ex 13536 ch2var 13541 bj-vtoclgf 13550 elabgf1 13553 bj-rspg 13561 sumdc2 13573 bdsepnf 13663 bj-nalset 13670 setindf 13741 strcollnf 13760 |
Copyright terms: Public domain | W3C validator |