mmtheorems13 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10658

Statement List for Metamath Proof Explorer - 1201-1300 - Page 13 of 107

Type	Label	Description
Statement
Theorem	sb4e 1201	One direction of a simplified definition of substitution that unlike sb4 1221 doesn't require a distinctor antecedent.
⊢ ([y / x]φ → ∀x(x = y → ∃yφ))
Theorem	hbsb2a 1202	Special case of a bound-variable hypothesis builder for substitution.
⊢ ([y / x]∀yφ → ∀x[y / x]φ)
Theorem	hbsb2e 1203	Special case of a bound-variable hypothesis builder for substitution.
⊢ ([y / x]φ → ∀x[y / x]∃yφ)
Theorem	hbsb3 1204	If y is not free in φ, x is not free in [y / x]φ.
⊢ (φ → ∀yφ)    ⇒   ⊢ ([y / x]φ → ∀x[y / x]φ)
Predicate calculus with distinct variables
The axiom of quantifier introduction ax-17
Theorem	a4imv 1205	A version of a4im 1157 with a distinct variable requirement instead of a bound variable hypothesis.
⊢ (x = y → (φ → ψ))    ⇒   ⊢ (∀xφ → ψ)
Theorem	aev 1206	A "distinctor elimination" lemma with no restrictions on variables in the consequent, proved without using ax-16 1208. The proof is unusual in that it involves linking 17 implications, which might provide an interesting challenge for an automated theorem prover.
⊢ (∀x x = y → ∀z w = v)
Derive the axiom of distinct variables ax-16
Theorem	ax16 1207	Theorem showing that ax-16 1208 is redundant if ax-17 969 is included in the axiom system. The important part of the proof is provided by aev 1206. See ax16ALT 1269 for an alternate proof that does not require ax-10 964 or ax-12 966. This theorem should not be referenced in any proof. Instead, use ax-16 1208 below so that theorems needing ax-16 1208 can be more easily identified.
⊢ (∀x x = y → (φ → ∀xφ))
Axiom	ax-16 1208	Axiom of Distinct Variables. The only axiom of predicate calculus requiring that variables be distinct (if we consider ax-17 969 to be a metatheorem and not an axiom). Axiom scheme C16' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases. It is a somewhat bizarre axiom since the antecedent is always false in set theory (see dtru 2767), but nonetheless it is technically necessary as you can see from its uses. This axiom is redundant if we include ax-17 969; see theorem ax16 1207. Alternately, ax-17 969 becomes logically redundant in the presence of this axiom, but without ax-17 969 we lose the more powerful metalogic that results from being able to express the concept of a set variable not occurring in a wff (as opposed to just two set variables being distinct). We retain ax-16 1208 here to provide logical completeness for systems with the simpler metalogic that results from omitting ax-17 969, which might be easier to study for some theoretical purposes.
⊢ (∀x x = y → (φ → ∀xφ))
Theorem	ax17eq 1209	Theorem to add distinct quantifier to atomic formula. (This theorem demonstrates the induction basis for ax-17 969 considered as a metatheorem. Do not use it for later proofs - use ax-17 969 instead, to avoid reference to the redundant axiom ax-16 1208.)
⊢ (x = y → ∀z x = y)
Theorem	dveeq2 1210	Quantifier introduction when one pair of variables is distinct.
⊢ (¬ ∀x x = y → (z = y → ∀x z = y))
Theorem	dveeq2ALT 1211	Version of dveeq2 1210 using ax-16 1208 instead of ax-17 969.
⊢ (¬ ∀x x = y → (z = y → ∀x z = y))
Theorem	19.23adv 1212	Deduction from Theorem 19.23 of [Margaris] p. 90.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃xψ → χ))
Theorem	ax11v2 1213	Recovery of ax11o 1215 from ax11v 1263 without using ax-11 965. The hypothesis is even weaker than ax11v 1263, with z both distinct from x and not occurring in φ. Thus the hypothesis provides an alternate axiom that can be used in place of ax11o 1215.
⊢ (x = z → (φ → ∀x(x = z → φ)))    ⇒   ⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
Theorem	ax11a2 1214	Derive ax-11o 1216 from a hypothesis in the form of ax-11 965. The hypothesis is even weaker than ax-11 965, with z both distinct from x and not occurring in φ. Thus the hypothesis provides an alternate axiom that can be used in place of ax11o 1215. As theorem ax11 1217 shows, the distinct variable conditions are optional. An open problem is whether ax11o 1215 can be derived from ax-11 965 without relying on ax-17 969.
⊢ (x = z → (∀zφ → ∀x(x = z → φ)))    ⇒   ⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
Derive the original axiom of variable substitution ax-11o
Theorem	ax11o 1215	Derivation of set.mm's original ax-11o 1216 from the shorter ax-11 965 that has replaced it. An open problem is whether this theorem can be proved without relying on ax-16 1208 or ax-17 969. Another open problem is whether this theorem can be proved without relying on ax-12 966 (see note in a12study 1376). Theorem ax11 1217 shows the reverse derivation of ax-11 965 from ax-11o 1216. This theorem should not be referenced in any proof. Instead, use ax-11o 1216 below so that theorems needing ax-11o 1216 can be more easily identified.
⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
Axiom	ax-11o 1216	Axiom ax-11o 1216 ("o" for "old") was the original version of ax-11 965, before it was discovered (in Jan. 2007) that the shorter ax-11 965 could replace it. It appears as Axiom scheme C15' in [Megill] p. 448 (p. 16 of the preprint). It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases. To understand this theorem more easily, think of "¬ ∀xx = y →..." as informally meaning "if x and y are distinct variables then..." The antecedent becomes false if the same variable is substituted for x and y, ensuring the theorem is sound whenever this is the case. In some later theorems, we call an antecedent of the form ¬ ∀xx = y a "distinctor." This axiom is redundant, as shown by theorem ax11o 1215.
⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
Theorem	ax11 1217	Rederivation of axiom ax-11 965 from the orginal version, ax-11o 1216. See theorem ax11o 1215 for the derivation of ax-11o 1216 from ax-11 965. This theorem should not be referenced in any proof. Instead, use ax-11 965 above so that uses of ax-11 965 can be more easily identified.
⊢ (x = y → (∀yφ → ∀x(x = y → φ)))
Theorems without distinct variables that use axiom ax-11o
Theorem	ax11b 1218	A bidirectional version of ax-11o 1216.
⊢ ((¬ ∀x x = y ⋀ x = y) → (φ ↔ ∀x(x = y → φ)))
Theorem	equs5 1219	Lemma used in proofs of substitution properties.
⊢ (¬ ∀x x = y → (∃x(x = y ⋀ φ) → ∀x(x = y → φ)))
Theorem	sb3 1220	One direction of a simplified definition of substitution when variables are distinct.
⊢ (¬ ∀x x = y → (∃x(x = y ⋀ φ) → [y / x]φ))
Theorem	sb4 1221	One direction of a simplified definition of substitution when variables are distinct.
⊢ (¬ ∀x x = y → ([y / x]φ → ∀x(x = y → φ)))
Theorem	sb4b 1222	Simplified definition of substitution when variables are distinct.
⊢ (¬ ∀x x = y → ([y / x]φ ↔ ∀x(x = y → φ)))
Theorem	dfsb2 1223	An alternate definition of proper substitution that, like df-sb 1170, mixes free and bound variables to avoid distinct variable requirements.
⊢ ([y / x]φ ↔ ((x = y ⋀ φ) ⋁ ∀x(x = y → φ)))
Theorem	dfsb3 1224	An alternate definition of proper substitution df-sb 1170 that uses only primitive connectives (no defined terms) on the right-hand side.
⊢ ([y / x]φ ↔ ((x = y → ¬ φ) → ∀x(x = y → φ)))
Theorem	hbsb2 1225	Bound-variable hypothesis builder for substitution.
⊢ (¬ ∀x x = y → ([y / x]φ → ∀x[y / x]φ))
Theorem	sbequi 1226	An equality theorem for substitution.
⊢ (x = y → ([x / z]φ → [y / z]φ))
Theorem	sbequ 1227	An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint).
⊢ (x = y → ([x / z]φ ↔ [y / z]φ))
Theorem	drsb2 1228	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).
⊢ (∀x x = y → ([x / z]φ ↔ [y / z]φ))
Theorem	sbn 1229	Negation inside and outside of substitution are equivalent.
⊢ ([y / x] ¬ φ ↔ ¬ [y / x]φ)
Theorem	sbi1 1230	Removal of implication from substitution.
⊢ ([y / x](φ → ψ) → ([y / x]φ → [y / x]ψ))
Theorem	sbi2 1231	Introduction of implication into substitution.
⊢ (([y / x]φ → [y / x]ψ) → [y / x](φ → ψ))
Theorem	sbim 1232	Implication inside and outside of substitution are equivalent.
⊢ ([y / x](φ → ψ) ↔ ([y / x]φ → [y / x]ψ))
Theorem	sbor 1233	Logical OR inside and outside of substitution are equivalent.
⊢ ([y / x](φ ⋁ ψ) ↔ ([y / x]φ ⋁ [y / x]ψ))
Theorem	sb19.21 1234	Substitution with a variable not free in antecedent affects only the consequent.
⊢ (φ → ∀xφ)    ⇒   ⊢ ([y / x](φ → ψ) ↔ (φ → [y / x]ψ))
Theorem	sban 1235	Conjunction inside and outside of a substitution are equivalent.
⊢ ([y / x](φ ⋀ ψ) ↔ ([y / x]φ ⋀ [y / x]ψ))
Theorem	sb3an 1236	Conjunction inside and outside of a substitution are equivalent.
⊢ ([y / x](φ ⋀ ψ ⋀ χ) ↔ ([y / x]φ ⋀ [y / x]ψ ⋀ [y / x]χ))
Theorem	sbbi 1237	Equivalence inside and outside of a substitution are equivalent.
⊢ ([y / x](φ ↔ ψ) ↔ ([y / x]φ ↔ [y / x]ψ))
Theorem	sblbis 1238	Introduce left biconditional inside of a substitution.
⊢ ([y / x]φ ↔ ψ)    ⇒   ⊢ ([y / x](χ ↔ φ) ↔ ([y / x]χ ↔ ψ))
Theorem	sbrbis 1239	Introduce right biconditional inside of a substitution.
⊢ ([y / x]φ ↔ ψ)    ⇒   ⊢ ([y / x](φ ↔ χ) ↔ (ψ ↔ [y / x]χ))
Theorem	sbrbif 1240	Introduce right biconditional inside of a substitution.
⊢ (χ → ∀xχ)    &   ⊢ ([y / x]φ ↔ ψ)    ⇒   ⊢ ([y / x](φ ↔ χ) ↔ (ψ ↔ χ))
Theorem	a4sbe 1241	A specialization theorem.
⊢ ([y / x]φ → ∃xφ)
Theorem	a4sbim 1242	Specialization of implication.
⊢ (∀x(φ → ψ) → ([y / x]φ → [y / x]ψ))
Theorem	a4sbbi 1243	Specialization of biconditional.
⊢ (∀x(φ ↔ ψ) → ([y / x]φ ↔ [y / x]ψ))
Theorem	sbbid 1244	Deduction substituting both sides of a biconditional.
⊢ (φ → ∀xφ)    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ([y / x]ψ ↔ [y / x]χ))
Theorem	sbequ8 1245	Elimination of equality from antecedent after substitution.
⊢ ([y / x]φ ↔ [y / x](x = y → φ))
Theorem	hbsb4 1246	A variable not free remains so after substitution with a distinct variable.
⊢ (φ → ∀zφ)    ⇒   ⊢ (¬ ∀z z = y → ([y / x]φ → ∀z[y / x]φ))
Theorem	hbsb4t 1247	A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1246).
⊢ (∀x∀z(φ → ∀zφ) → (¬ ∀z z = y → ([y / x]φ → ∀z[y / x]φ)))
Theorem	dvelimf 1248	Version of dvelim 1350 without any variable restrictions.
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀zψ)    &   ⊢ (z = y → (φ ↔ ψ))    ⇒   ⊢ (¬ ∀x x = y → (ψ → ∀xψ))
Theorem	dvelimdf 1249	Deduction form of dvelimf 1248. This version may be useful if we want to avoid ax-17 969 and use ax-16 1208 instead.
⊢ (φ → ∀xφ)    &   ⊢ (φ → ∀zφ)    &   ⊢ (φ → (ψ → ∀xψ))    &   ⊢ (φ → (χ → ∀zχ))    &   ⊢ (φ → (z = y → (ψ ↔ χ)))    ⇒   ⊢ (φ → (¬ ∀x x = y → (χ → ∀xχ)))
Theorem	sbco 1250	A composition law for substitution.
⊢ ([y / x][x / y]φ ↔ [y / x]φ)
Theorem	sbid2 1251	An identity law for substitution.
⊢ (φ → ∀xφ)    ⇒   ⊢ ([y / x][x / y]φ ↔ φ)
Theorem	sbidm 1252	An idempotent law for substitution.
⊢ ([y / x][y / x]φ ↔ [y / x]φ)
Theorem	sbco2 1253	A composition law for substitution.
⊢ (φ → ∀zφ)    ⇒   ⊢ ([y / z][z / x]φ ↔ [y / x]φ)
Theorem	sbco2d 1254	A composition law for substitution.
⊢ (φ → ∀xφ)    &   ⊢ (φ → ∀zφ)    &   ⊢ (φ → (ψ → ∀zψ))    ⇒   ⊢ (φ → ([y / z][z / x]ψ ↔ [y / x]ψ))
Theorem	sbco3 1255	A composition law for substitution.
⊢ ([z / y][y / x]φ ↔ [z / x][x / y]φ)
Theorem	sbcom 1256	A commutativity law for substitution.
⊢ ([y / z][y / x]φ ↔ [y / x][y / z]φ)
Theorem	sb5rf 1257	Reversed substitution.
⊢ (φ → ∀yφ)    ⇒   ⊢ (φ ↔ ∃y(y = x ⋀ [y / x]φ))
Theorem	sb6rf 1258	Reversed substitution.
⊢ (φ → ∀yφ)    ⇒   ⊢ (φ ↔ ∀y(y = x → [y / x]φ))
Theorem	sb8 1259	Substitution of variable in universal quantifier.
⊢ (φ → ∀yφ)    ⇒   ⊢ (∀xφ ↔ ∀y[y / x]φ)
Theorem	sb8e 1260	Substitution of variable in existential quantifier.
⊢ (φ → ∀yφ)    ⇒   ⊢ (∃xφ ↔ ∃y[y / x]φ)
Theorem	sb9i 1261	Commutation of quantification and substitution variables.
⊢ (∀x[x / y]φ → ∀y[y / x]φ)
Theorem	sb9 1262	Commutation of quantification and substitution variables.
⊢ (∀x[x / y]φ ↔ ∀y[y / x]φ)
Predicate calculus with distinct variables (cont.)
Theorem	ax11v 1263	This is a version of ax-11o 1216 when the variables are distinct. Axiom (C8) of [Monk2] p. 105. See theorem ax11v2 1213 for the rederivation of ax-11o 1216 from this theorem.
⊢ (x = y → (φ → ∀x(x = y → φ)))
Theorem	sb56 1264	Two equivalent ways of expressing the proper substitution of y for x in φ, when x and y are distinct. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 1170.
⊢ (∃x(x = y ⋀ φ) ↔ ∀x(x = y → φ))
Theorem	sb6 1265	Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70.
⊢ ([y / x]φ ↔ ∀x(x = y → φ))
Theorem	sb5 1266	Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40.
⊢ ([y / x]φ ↔ ∃x(x = y ⋀ φ))
Theorem	equid1 1267	Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68. This proof is similar to Tarski's and makes use of a dummy variable y. See equid 1124 for a proof that avoids dummy variables (but is less intuitive).
⊢ x = x
Theorem	ax16i 1268	Inference with ax-16 1208 as its conclusion, that doesn't require ax-10 964, ax-11 965, or ax-12 966 for its proof. The hypotheses may be eliminable without one or more of these axioms in special cases.
⊢ (x = z → (φ ↔ ψ))    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ (∀x x = y → (φ → ∀xφ))
Theorem	ax16ALT 1269	Version of ax16 1207 that doesn't require ax-10 964 or ax-12 966 for its proof.
⊢ (∀x x = y → (φ → ∀xφ))
Theorem	a4v 1270	Specialization with implicit substitution.
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∀xφ → ψ)
Theorem	a4imev 1271	Distinct-variable version of a4ime 1158.
⊢ (x = y → (φ → ψ))    ⇒   ⊢ (φ → ∃xψ)
Theorem	a4eiv 1272	Inference from existential specialization with implicit substitution.
⊢ (x = y → (φ ↔ ψ))    &   ⊢ ψ    ⇒   ⊢ ∃xφ
Theorem	equvin 1273	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109.
⊢ (x = y ↔ ∃z(x = z ⋀ z = y))
Theorem	a16g 1274	A generalization of axiom ax-16 1208.
⊢ (∀x x = y → (φ → ∀zφ))
Theorem	a16gb 1275	A generalization of axiom ax-16 1208.
⊢ (∀x x = y → (φ ↔ ∀zφ))
Theorem	albidv 1276	Formula-building rule for universal quantifier (deduction rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀xψ ↔ ∀xχ))
Theorem	exbidv 1277	Formula-building rule for existential quantifier (deduction rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃xψ ↔ ∃xχ))
Theorem	2albidv 1278	Formula-building rule for 2 existential quantifiers (deduction rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀x∀yψ ↔ ∀x∀yχ))
Theorem	2exbidv 1279	Formula-building rule for 2 existential quantifiers (deduction rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x∃yψ ↔ ∃x∃yχ))
Theorem	3exbidv 1280	Formula-building rule for 3 existential quantifiers (deduction rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x∃y∃zψ ↔ ∃x∃y∃zχ))
Theorem	4exbidv 1281	Formula-building rule for 4 existential quantifiers (deduction rule).
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃x∃y∃z∃wψ ↔ ∃x∃y∃z∃wχ))
Theorem	19.9v 1282	Special case of Theorem 19.9 of [Margaris] p. 89.
⊢ (∃xφ ↔ φ)
Theorem	19.21v 1283	Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as (φ → ∀xφ) in 19.21 1054 via the use of distinct variable conditions combined with ax-17 969. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g. euf 1382 derived from df-eu 1380. The "f" stands for "not free in" which is less restrictive than "does not occur in."
⊢ (∀x(φ → ψ) ↔ (φ → ∀xψ))
Theorem	19.21aiv 1284	Inference from Theorem 19.21 of [Margaris] p. 90.
⊢ (φ → ψ)    ⇒   ⊢ (φ → ∀xψ)
Theorem	19.21aivv 1285	Inference from Theorem 19.21 of [Margaris] p. 90.
⊢ (φ → ψ)    ⇒   ⊢ (φ → ∀x∀yψ)
Theorem	19.21adv 1286	Deduction from Theorem 19.21 of [Margaris] p. 90.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (ψ → ∀xχ))
Theorem	19.20dv 1287	Deduction from Theorem 19.20 of [Margaris] p. 90.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∀xψ → ∀xχ))
Theorem	19.22dv 1288	Deduction from Theorem 19.22 of [Margaris] p. 90.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃xψ → ∃xχ))
Theorem	19.20dvv 1289	Deduction from Theorem 19.22 of [Margaris] p. 90.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∀x∀yψ → ∀x∀yχ))
Theorem	19.22dvv 1290	Deduction from Theorem 19.22 of [Margaris] p. 90.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃x∃yψ → ∃x∃yχ))
Theorem	19.23v 1291	Special case of Theorem 19.23 of [Margaris] p. 90.
⊢ (∀x(φ → ψ) ↔ (∃xφ → ψ))
Theorem	19.23vv 1292	Theorem 19.23 of [Margaris] p. 90 extended to two variables.
⊢ (∀x∀y(φ → ψ) ↔ (∃x∃yφ → ψ))
Theorem	19.23aiv 1293	Inference from Theorem 19.23 of [Margaris] p. 90.
⊢ (φ → ψ)    ⇒   ⊢ (∃xφ → ψ)
Theorem	19.23aivv 1294	Inference from Theorem 19.23 of [Margaris] p. 90.
⊢ (φ → ψ)    ⇒   ⊢ (∃x∃yφ → ψ)
Theorem	19.23advv 1295	Deduction from Theorem 19.23 of [Margaris] p. 90.
⊢ (φ → (ψ → χ))    ⇒   ⊢ (φ → (∃x∃yψ → χ))
Theorem	19.27v 1296	Theorem 19.27 of [Margaris] p. 90.
⊢ (∀x(φ ⋀ ψ) ↔ (∀xφ ⋀ ψ))
Theorem	19.28v 1297	Theorem 19.28 of [Margaris] p. 90.
⊢ (∀x(φ ⋀ ψ) ↔ (φ ⋀ ∀xψ))
Theorem	19.36v 1298	Special case of Theorem 19.36 of [Margaris] p. 90.
⊢ (∃x(φ → ψ) ↔ (∀xφ → ψ))
Theorem	19.36aiv 1299	Inference from Theorem 19.36 of [Margaris] p. 90.
⊢ ∃x(φ → ψ)    ⇒   ⊢ (∀xφ → ψ)
Theorem	19.12vv 1300	Special case of 19.12 1045 where its converse holds.
⊢ (∃x∀y(φ → ψ) ↔ ∀y∃x(φ → ψ))