Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sps | GIF version |
Description: Generalization of antecedent. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sps.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
sps | ⊢ (∀𝑥𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sp 1498 | . 2 ⊢ (∀𝑥𝜑 → 𝜑) | |
2 | sps.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | syl 14 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1340 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-4 1497 |
This theorem is referenced by: 19.21ht 1568 exim 1586 alexdc 1606 19.2 1625 ax10o 1702 hbae 1705 cbv1h 1733 equvini 1745 equveli 1746 ax10oe 1784 drex1 1785 drsb1 1786 exdistrfor 1787 ax11v2 1807 equs5or 1817 sbequi 1826 drsb2 1828 spsbim 1830 sbcomxyyz 1959 hbsb4t 2000 mopick 2091 eupickbi 2095 ceqsalg 2749 mo2icl 2900 reu6 2910 sbcal 2997 csbie2t 3088 dfss4st 3350 reldisj 3455 dfnfc2 3801 ssopab2 4247 eusvnfb 4426 mosubopt 4663 issref 4980 fv3 5503 fvmptt 5571 fnoprabg 5934 bj-exlimmp 13491 strcollnft 13707 |
Copyright terms: Public domain | W3C validator |