P. 10 of Theorem List - bfol.mm Proof Explorer

Theorem List for bfol.mm Proof Explorer - 901-1000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ndsubmultl-P7.24d.RC 901	Inference Form of ndsubmultl-P7.24d 854. †
⊢ 𝑡 = 𝑢    ⇒   ⊢ (𝑡 ⋅ 𝑤) = (𝑢 ⋅ 𝑤)
Theorem	ndsubmultr-P7.24e.RC 902	Inference Form of ndsubmultr-P7.24e 855. †
⊢ 𝑡 = 𝑢    ⇒   ⊢ (𝑤 ⋅ 𝑡) = (𝑤 ⋅ 𝑢)
Theorem	ndsubmultd-P7.RC 903	Inference Form of ndsubmultd-P7 859. †
⊢ 𝑠 = 𝑡    &   ⊢ 𝑢 = 𝑤    ⇒   ⊢ (𝑠 ⋅ 𝑢) = (𝑡 ⋅ 𝑤)
8.1.2.4  Closed Forms of Natural Deduction Rules.
Theorem	ndnfrneg-P7.2.CL 904	Closed Form of ndnfrneg-P7.2 827. †
⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
Theorem	ndnfrim-P7.3.CL 905	Closed Form of ndnfrim-P7.3 828. †
⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 → 𝜓))
Theorem	ndnfrand-P7.4.CL 906	Closed Form of ndnfrand-P7.4 829. †
⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 ∧ 𝜓))
Theorem	ndnfror-P7.5.CL 907	Closed Form of ndnfror-P7.5 830. †
⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 ∨ 𝜓))
Theorem	ndnfrbi-P7.6.CL 908	Closed Form of ndnfrbi-P7.6 831. †
⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 ↔ 𝜓))
Theorem	ndalle-P7.18.CL 909	Closed Form of ndalle-P7.18 843. †
⊢ (∀𝑥𝜑 → [𝑡 / 𝑥]𝜑)
Theorem	ndexi-P7.19.CL 910	Closed Form of ndexi-P7.19 844. †
⊢ ([𝑡 / 𝑥]𝜑 → ∃𝑥𝜑)
Theorem	ndsubeql-P7.22a.CL 911	Closed Form of ndsubeql-P7.22a 847. †
⊢ (𝑡 = 𝑢 → (𝑡 = 𝑤 ↔ 𝑢 = 𝑤))
Theorem	ndsubeqr-P7.22b.CL 912	Closed Form of ndsubeqr-P7.22b 848. †
⊢ (𝑡 = 𝑢 → (𝑤 = 𝑡 ↔ 𝑤 = 𝑢))
Theorem	ndsubeqd-P7.CL 913	Closed Form of ndsubeqd-P7 856. †
⊢ ((𝑠 = 𝑡 ∧ 𝑢 = 𝑤) → (𝑠 = 𝑢 ↔ 𝑡 = 𝑤))
Theorem	ndsubelofl-P7.23a.CL 914	Closed Form of ndsubelofl-P7.23a 849. †
⊢ (𝑡 = 𝑢 → (𝑡 ∈ 𝑤 ↔ 𝑢 ∈ 𝑤))
Theorem	ndsubelofr-P7.23b.CL 915	Closed Form of ndsubelofr-P7.23b 850. †
⊢ (𝑡 = 𝑢 → (𝑤 ∈ 𝑡 ↔ 𝑤 ∈ 𝑢))
Theorem	ndsubelofd-P7.CL 916	Closed Form of ndsubelofd-P7 857. †
⊢ ((𝑠 = 𝑡 ∧ 𝑢 = 𝑤) → (𝑠 ∈ 𝑢 ↔ 𝑡 ∈ 𝑤))
Theorem	ndsubsucc-P7.24a.CL 917	Closed Form of ndsubsucc-P7.24a 851. †
⊢ (𝑡 = 𝑢 → s‘𝑡 = s‘𝑢)
Theorem	ndsubaddl-P7.24b.CL 918	Closed Form of ndsubaddl-P7.24b 852. †
⊢ (𝑡 = 𝑢 → (𝑡 + 𝑤) = (𝑢 + 𝑤))
Theorem	ndsubaddr-P7.24c.CL 919	Closed Form of ndsubaddr-P7.24c 853. †
⊢ (𝑡 = 𝑢 → (𝑤 + 𝑡) = (𝑤 + 𝑢))
Theorem	ndsubaddd-P7.CL 920	Closed Form of ndsubaddd-P7 858. †
⊢ ((𝑠 = 𝑡 ∧ 𝑢 = 𝑤) → (𝑠 + 𝑢) = (𝑡 + 𝑤))
Theorem	ndsubmultl-P7.24d.CL 921	Closed Form of ndsubmultl-P7.24d 854. †
⊢ (𝑡 = 𝑢 → (𝑡 ⋅ 𝑤) = (𝑢 ⋅ 𝑤))
Theorem	ndsubmultr-P7.24e.CL 922	Closed Form of ndsubmultr-P7.24e 855. †
⊢ (𝑡 = 𝑢 → (𝑤 ⋅ 𝑡) = (𝑤 ⋅ 𝑢))
Theorem	ndsubmultd-P7.CL 923	Closed Form of ndsubmultd-P7 859. †
⊢ ((𝑠 = 𝑡 ∧ 𝑢 = 𝑤) → (𝑠 ⋅ 𝑢) = (𝑡 ⋅ 𝑤))
8.2  Recovering Hilbert Axioms and Definitions.
8.2.1  Axiom L6 (Existential Form).
Theorem	lemma-L7.01a 924*	Proper Substitution Over Equality Lemma. † '𝑥' cannot occur in '𝑡' or '𝑢'.
⊢ ([𝑡 / 𝑥] 𝑥 = 𝑢 ↔ 𝑡 = 𝑢)
8.2.1.1  Recovered Axiom L6 (Existential Form).
Theorem	axL6ex-P7 925*	Existential Form of ax-L6 18, Derived from Natural Deduction Rules. † '𝑥' cannot occur in '𝑡'.
⊢ ∃𝑥 𝑥 = 𝑡
8.2.2  Generalization Rule and Axiom L5.
Theorem	nfrthm-P7 926	Every Variable is ENF in a Theorem. †
⊢ 𝜑    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	psubnfrv-P7 927*	Proper Substitution Applied To ENF Variable (variable restriction). † '𝑥' cannot occur in '𝑡'.
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑡 / 𝑥]𝜑 ↔ 𝜑)
Theorem	nfrgen-P7 928	ENF In ⇒ General For. †
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → ∀𝑥𝜑)
Theorem	nfrgen-P7.RC 929	Inference Form of nfrgen-P7 928. †
⊢ Ⅎ𝑥𝜑    &   ⊢ 𝜑    ⇒   ⊢ ∀𝑥𝜑
Theorem	nfrgen-P7.CL 930	Closed Form of nfrgen-P7 928. †
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝜑 → ∀𝑥𝜑)
Theorem	nfrexgen-P7 931	Dual Form of nfrgen-P7 928. †
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	nfrexgen-P7.CL 932	Closed Form of nfrexgen-P7 931. †
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (∃𝑥𝜑 → 𝜑)
8.2.2.1  Recovered Generalization Rule.
Theorem	axGEN-P7 933	Generalization Rule (ax-GEN 15), Derived from Natural Deduction Rules. †
⊢ 𝜑    ⇒   ⊢ ∀𝑥𝜑
8.2.2.2  Recovered Axiom L5.
Theorem	axL5-P7 934*	ax-L5 17 Derived from Natural Deduction Rules. †
⊢ (𝜑 → ∀𝑥𝜑)
Theorem	axL5ex-P7 935*	Existential Form of axL5-P7 934. †
⊢ (∃𝑥𝜑 → 𝜑)
8.2.3  Axiom L4.
Theorem	eqsym-P7 936	Equivalence Property: '=' Symmetry. †
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → 𝑢 = 𝑡)
Theorem	eqsym-P7.CL 937	Closed Form of eqsym-P7 936. †
⊢ (𝑡 = 𝑢 → 𝑢 = 𝑡)
Theorem	eqsym-P7.CL.SYM 938	Closed Symmetric Form of eqsym-P7 936. †
⊢ (𝑡 = 𝑢 ↔ 𝑢 = 𝑡)
Theorem	psubinv-P7 939*	Proper Substitution Inverse Property. †
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ ([𝑥 / 𝑦][𝑦 / 𝑥]𝜑 ↔ 𝜑)
Theorem	psubid-P7 940	Proper Substitution Identity Property. †
⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
Theorem	alle-P7 941	Simplified '∀' Elimination Law. † This is also known as the Specialization Law. For the original form, using explicit substitution, see ndalle-P7.18 843.
⊢ (𝛾 → ∀𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	alle-P7.CL 942	Closed Form of alle-P7 941. †
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	lemma-L7.02a-L1 943*	Lemma for lemma-L7.02a 944. † [Auxiliary lemma - not displayed.]
Theorem	lemma-L7.02a 944	Proper Substitution Over Implication Lemma. †
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → ([𝑡 / 𝑥]𝜑 → [𝑡 / 𝑥]𝜓))
8.2.3.1  Recovered Axiom L4.
Theorem	axL4-P7 945	ax-L4 16 Derived from Natural Deduction Rules. †
⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	axL4ex-P7 946	Existential Form of axL4-P7 945. †
⊢ (∀𝑥(𝜑 → 𝜓) → (∃𝑥𝜑 → ∃𝑥𝜓))
8.2.4  Existential Quantifier
Theorem	alli-P7 947	Simplified '∀' Introduction Law. † For the original form, using explicit substitution, see ndalli-P7.17 842. The inference form is axGEN-P7 933.
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → ∀𝑥𝜑)
Theorem	alloverimex-P7 948	Alternate version of alloverim-P7 970 that produces existential quantifiers. †
⊢ (𝛾 → ∀𝑥(𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	alloverimex-P7.GENF 949	alloverimex-P7 948 with generalization augmentation (non-freeness condition). †
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → ∃𝑥𝜓))
Theorem	alloverimex-P7.GENF.RC 950	Inference Form of alloverimex-P7.GENF 949. †
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → ∃𝑥𝜓)
Theorem	exi-P7 951	Simplified '∃' Introduction Law. † For the original form, using explicit substitution, see ndalli-P7.17 842.
⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → ∃𝑥𝜑)
Theorem	exi-P7.CL 952	Closed Form of exi-P7 951. †
⊢ (𝜑 → ∃𝑥𝜑)
Theorem	exia-P7 953	Introduce Existential Quantifier as Antecedent. †
⊢ Ⅎ𝑥𝛾    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∃𝑥𝜑 → 𝜓))
Theorem	exia-P7.RC 954	Inference Form of exia-P7 953. †
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	exe-P7 955	Simplified '∃' Elimination Law. † For the original form, using explicit substitution, see ndexe-P7.20 845.
⊢ Ⅎ𝑥𝛾    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	allnegex-P7-L1 956	Lemma for allnegex-P7 958. † [Auxiliary lemma - not displayed.]
Theorem	allnegex-P7-L2 957	Lemma for allnegex-P7 958. † [Auxiliary lemma - not displayed.]
Theorem	allnegex-P7 958	"For all not" is Equivalent to "Does not exist". † This statement is deducible with intuitionist logic. It's dual, given by exnegall-P7 1046, is not.
⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
8.2.4.1  Recovered Existential Quantifier Definition. In intuitionist logic, existential quantification is a stronger notion than in the classical case as we have '(∃𝑥𝜑 → ¬ ∀𝑥¬ 𝜑)', but not '(¬ ∀𝑥¬ 𝜑 → ∃𝑥𝜑)'. Also, unlike in the classical case, there is also no closed formula for existential quantification in terms of other the other primitive symbols.
Theorem	dfexists-P7 959	df-exists-D5.1 596 Derived from Natural Deduction Rules. Note that this definition is not deducible with intuitionist logic.
⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
Theorem	dfexistsint-P7 960	Necessary Condition for (i.e. "If" part of) Existential Quantifier Definition. Only this direction is deducible with intuitionist logic. †
⊢ (∃𝑥𝜑 → ¬ ∀𝑥 ¬ 𝜑)
8.2.4.2  Recovered Axiom L6 (Original Form). In intuitionist logic, the original form of Axiom L6, given here as axL6-P7 961, is weaker than the form involving existential quantification, deduced earlier as axL6ex-P7 925.
Theorem	axL6-P7 961*	ax-L6 18 Derived From Natural Deduction Rules. † '𝑥' cannot occur in '𝑡'.
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑡
8.2.5  Effective Non-Freeness.
Theorem	lemma-L7.03 962*	Proper Substitution Applied To ENF Variable Lemma. † '𝑥' cannot occur in '𝑡'.
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → Ⅎ𝑥𝜑)    ⇒   ⊢ (𝛾 → ([𝑡 / 𝑥]𝜑 ↔ 𝜑))
Theorem	gennfrcl-P7 963	General for ⇒ ENF in (closed form). †
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
Theorem	dfnfreealtif-P7 964	Necessary Condition for (i.e. "If" part of) Alternate ENF Definition. †
⊢ ((∃𝑥𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
Theorem	nfrgencl-P7 965	ENF In ⇒ General For (closed form). †
⊢ (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑))
Theorem	dfnfreealtonlyif-P7 966	Sufficient Condition for (i.e. "Only If" part of) Alternate ENF Definition . †
⊢ (Ⅎ𝑥𝜑 → (∃𝑥𝜑 → ∀𝑥𝜑))
8.2.5.1  Recovered Alternate ENF Definition.
Theorem	dfnfreealt-P7 967	dfnfreealt-P6 683 Derived from Natural Deduction Rules. †
⊢ (Ⅎ𝑥𝜑 ↔ (∃𝑥𝜑 → ∀𝑥𝜑))
8.2.5.2  Recovered ENF Definition. In intuitionist logic, we see that dfnfreealt-P6 683 is the closed formula for effective non-freeness, and the notion defined by dfnfree-P7 968 is too strong.
Theorem	dfnfree-P7 968	df-nfree-D6.1 682 Derived From Natural Deduction Rules. This definition is not valid with intuitionist logic.
⊢ (Ⅎ𝑥𝜑 ↔ (∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑))
Theorem	dfnfreeint-P7 969	Necessary Condition for (i.e. "If" part of) df-nfree-D6.1 682 Derived From Natural Deduction Rules. † Only this direction is deducible with intuitionist logic.
⊢ ((∀𝑥𝜑 ∨ ∀𝑥 ¬ 𝜑) → Ⅎ𝑥𝜑)
8.2.6  Proper Substitution.
Theorem	alloverim-P7 970	'∀' Distributes Over '→'. †
⊢ (𝛾 → ∀𝑥(𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	alloverim-P7.GENF 971	alloverim-P7 970 with generalization augmentation (non-freeness condition). †
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 → 𝜓))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	alloverim-P7.GENF.RC 972	Inference Form of alloverim-P7.GENF 971. †
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	suball-P7 973	Substitution Theorem for '∀𝑥' (non-freeness condition). †
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (𝛾 → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
Theorem	suball-P7.RC 974	Inference Form of suball-P7.RC 974. †
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Theorem	qimeqallhalf-P7 975	Partial Quantified Implication Equivalence Law ( ( E → U ) → U ). † The reverse implication is also true if '𝑥' is ENF in either '𝜑' (see qimeqalla-P7 1050) or '𝜓' (see qimeqallb-P7r 1052).
⊢ ((∃𝑥𝜑 → ∀𝑥𝜓) → ∀𝑥(𝜑 → 𝜓))
Theorem	qimeqallb-P7 976	Quantified Implication Equivalence Law ( U ↔ ( E → U ) ) (non-freeness condition b). †
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑥𝜓))
8.2.6.1  Recovered Simplified Proper Substitution Definition.
Theorem	dfpsubv-P7 977*	dfpsubv-P6 717, Derived from Natural Deduction Rules (restriction on '𝑡'). † This form can be used whenever '𝑥' does not occur in '𝑡'.
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑))
8.2.6.2  Recovered Full Proper Substitution Definition.
Theorem	dfpsub-P7 978*	df-psub-D6.2 716, Derived from Natural Deduction Rules. †
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
8.2.7  Scheme Completion Axioms.
8.2.7.1  Recovered Axiom L10.
Theorem	axL10-P7 979	ax-L10 27 Derived from Natural Deduction Rules. †
⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑)
8.2.7.2  Recovered Axiom L11.
Theorem	axL11-P7 980*	ax-L11 28 Derived from Natural Deduction Rules. †
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	axL11ex-P7 981*	Existential Form of axL11-P7 980. †
⊢ (∃𝑥∃𝑦𝜑 → ∃𝑦∃𝑥𝜑)
8.2.7.3  Recovered Axiom L12.
Theorem	axL12-P7 982*	ax-L12 29 Derived from Natural Deduction Rules. † '𝑥' cannot occur in '𝑡'.
⊢ (𝑥 = 𝑡 → (𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)))
8.3  Revisiting Chapter 5.
8.3.1  Equivalence Properties of Equality Predicate. Show that '=' is an equivalence relation. Reflexivity is given by ndeqi-P7.21 846.
Theorem	eqsym-P7r 983	Equivalence Property: '=' Symmetry. † This is the restatement of a previously proven result. Do not use in proofs. Use eqsym-P7 936 instead.
⊢ (𝛾 → 𝑡 = 𝑢)    ⇒   ⊢ (𝛾 → 𝑢 = 𝑡)
Theorem	eqsym-P7r.RC 984	Inference Form of eqsym-P7r 983. †
⊢ 𝑡 = 𝑢    ⇒   ⊢ 𝑢 = 𝑡
Theorem	eqsym-P7r.CL 985	Closed Form of eqsym-P7r 983. † This is the restatement of a previously proven result. Do not use in proofs. Use eqsym-P7 936 instead.
⊢ (𝑡 = 𝑢 → 𝑢 = 𝑡)
Theorem	eqsym-P7r.CL.SYM 986	Closed Symmetric Form of eqsym-P7r 983. † This is the restatement of a previously proven result. Do not use in proofs. Use eqsym-P7 936 instead.
⊢ (𝑡 = 𝑢 ↔ 𝑢 = 𝑡)
Theorem	eqtrns-P7 987	Equivalence Property: '=' Transitivity. †
⊢ (𝛾 → 𝑡 = 𝑢)    &   ⊢ (𝛾 → 𝑢 = 𝑤)    ⇒   ⊢ (𝛾 → 𝑡 = 𝑤)
Theorem	eqtrns-P7.RC 988	Inference Form of eqtrns-P7 987. †
⊢ 𝑡 = 𝑢    &   ⊢ 𝑢 = 𝑤    ⇒   ⊢ 𝑡 = 𝑤
Theorem	eqtrns-P7.CL 989	Closed Form of eqtrns-P7 987. †
⊢ ((𝑡 = 𝑢 ∧ 𝑢 = 𝑤) → 𝑡 = 𝑤)
8.3.2  Simplified Quantifier Introduction / Elimination Rules.
Theorem	alli-P7r 990	Simplified '∀' Introduction Law. † For the original form, using explicit substitution, see ndalli-P7.17 842. The inference form is axGEN-P7 933. This is the restatement of a previously proven result. Do not use in proofs. Use alli-P7 947 instead.
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → ∀𝑥𝜑)
Theorem	alli-P7r.VR 991*	alli-P7r 990 with variable restriction. † '𝑥' cannot occur in '𝛾'.
⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → ∀𝑥𝜑)
Theorem	alle-P7r 992	Simplified '∀' Elimination Law. † This is also known as the Specialization Law. For the original form, using explicit substitution, see ndalle-P7.18 843. This is the restatement of a previously proven result. Do not use in proofs. Use alle-P7 941 instead.
⊢ (𝛾 → ∀𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜑)
Theorem	alle-P7r.RC 993	Inference Form of alle-P7r 992. †
⊢ ∀𝑥𝜑    ⇒   ⊢ 𝜑
Theorem	alle-P7r.CL 994	Closed Form of alle-P7r 992. † This is the restatement of a previously proven result. Do not use in proofs. Use alle-P7.CL 942 instead.
⊢ (∀𝑥𝜑 → 𝜑)
Theorem	exi-P7r 995	Simplified '∃' Introduction Law. † For the original form, using explicit substitution, see ndexi-P7.19 844. This is the restatement of a previously proven result. Do not use in proofs. Use exi-P7 951 instead.
⊢ (𝛾 → 𝜑)    ⇒   ⊢ (𝛾 → ∃𝑥𝜑)
Theorem	exi-P7r.RC 996	Inference Form of exi-P7r 995. †
⊢ 𝜑    ⇒   ⊢ ∃𝑥𝜑
Theorem	exi-P7r.CL 997	Closed Form of exi-P7r 995. † This is the restatement of a previously proven result. Do not use in proofs. Use exi-P7.CL 952 instead.
⊢ (𝜑 → ∃𝑥𝜑)
Theorem	exe-P7r 998	Simplified '∃' Elimination Law. † For the original form, using explicit substitution, see ndexe-P7.20 845 and ndexew-P7 867. This is the restatement of a previously proven result. Do not use in proofs. Use exe-P7 955 instead.
⊢ Ⅎ𝑥𝛾    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	exe-P7r.VR1of2 999*	exe-P7r 998 with one variable restriction. † '𝑥' cannot occur in '𝛾'.
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)
Theorem	exe-P7r.VR2of2 1000*	exe-P7r 998 with one variable restriction. '𝑥' cannot occur in '𝜓'.
⊢ Ⅎ𝑥𝛾    &   ⊢ (𝛾 → (𝜑 → 𝜓))    &   ⊢ (𝛾 → ∃𝑥𝜑)    ⇒   ⊢ (𝛾 → 𝜓)