mmtheorems11 - 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-10686

Statement List for Metamath Proof Explorer - 1001-1100 - Page 11 of 107

Type	Label	Description
Statement
Theorem	hba1 1001	x is not free in A.xph. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114.
|- (A.xph -> A.xA.xph)
Theorem	hbn 1002	If x is not free in ph, it is not free in -. ph.
|- (ph -> A.xph)   =>   |- (-. ph -> A.x -. ph)
Theorem	hbal 1003	If x is not free in ph, it is not free in A.yph.
|- (ph -> A.xph)   =>   |- (A.yph -> A.xA.yph)
Theorem	hbex 1004	If x is not free in ph, it is not free in E.yph.
|- (ph -> A.xph)   =>   |- (E.yph -> A.xE.yph)
Theorem	hbim 1005	If x is not free in ph and ps, it is not free in (ph -> ps). (The proof was shortened by O'Cat, 3-Mar-2008.)
|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph -> ps) -> A.x(ph -> ps))
Theorem	hbor 1006	If x is not free in ph and ps, it is not free in (ph \/ ps).
|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph \/ ps) -> A.x(ph \/ ps))
Theorem	hban 1007	If x is not free in ph and ps, it is not free in (ph /\ ps).
|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph /\ ps) -> A.x(ph /\ ps))
Theorem	hbbi 1008	If x is not free in ph and ps, it is not free in (ph <-> ps).
|- (ph -> A.xph)   &   |- (ps -> A.xps)   =>   |- ((ph <-> ps) -> A.x(ph <-> ps))
Theorem	hb3or 1009	If x is not free in ph, ps, and ch, it is not free in (ph \/ ps \/ ch).
|- (ph -> A.xph)   &   |- (ps -> A.xps)   &   |- (ch -> A.xch)   =>   |- ((ph \/ ps \/ ch) -> A.x(ph \/ ps \/ ch))
Theorem	hb3an 1010	If x is not free in ph, ps, and ch, it is not free in (ph /\ ps /\ ch).
|- (ph -> A.xph)   &   |- (ps -> A.xps)   &   |- (ch -> A.xch)   =>   |- ((ph /\ ps /\ ch) -> A.x(ph /\ ps /\ ch))
Theorem	hba2 1011	Lemma 24 of [Monk2] p. 114.
|- (A.yA.xph -> A.xA.yA.xph)
Theorem	hbia1 1012	Lemma 23 of [Monk2] p. 114.
|- ((A.xph -> A.xps) -> A.x(A.xph -> A.xps))
Theorem	hbn1 1013	x is not free in -. A.xph.
|- (-. A.xph -> A.x -. A.xph)
Theorem	hbe1 1014	x is not free in E.xph.
|- (E.xph -> A.xE.xph)
Theorem	ax46 1015	Proof of a single axiom that can replace ax-4 971 and ax-6o 976. See ax46to4 1016 and ax46to6 1017 for the re-derivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.)
|- ((A.x -. A.xph -> A.xph) -> ph)
Theorem	ax46to4 1016	Re-derivation of ax-4 971 from ax46 1015. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.)
|- (A.xph -> ph)
Theorem	ax46to6 1017	Re-derivation of ax-6o 976 from ax46 1015. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.)
|- (-. A.x -. A.xph -> ph)
Theorem	ax67 1018	Proof of a single axiom that can replace both ax-6o 976 and ax-7 960. See ax67to6 1019 and ax67to7 1020 for the re-derivation of those axioms.
|- (-. A.x -. A.yA.xph -> A.yph)
Theorem	ax67to6 1019	Re-derivation of ax-6o 976 from ax67 1018. Note that ax-6o 976 and ax-7 960 are not used by the re-derivation.
|- (-. A.x -. A.xph -> ph)
Theorem	ax67to7 1020	Re-derivation of ax-7 960 from ax67 1018. Note that ax-6o 976 and ax-7 960 are not used by the re-derivation.
|- (A.xA.yph -> A.yA.xph)
Theorem	ax467 1021	Proof of a single axiom that can replace ax-4 971, ax-6o 976, and ax-7 960 in a subsystem that includes these axioms plus ax-5o 973 and ax-gen 961 (and propositional calculus). See ax467to4 1022, ax467to6 1023, and ax467to7 1024 for the re-derivation of those axioms. This theorem extends the idea in Scott Fenton's ax46 1015.
|- ((A.xA.y -. A.xA.yph -> A.xph) -> ph)
Theorem	ax467to4 1022	Re-derivation of ax-4 971 from ax467 1021. Only propositional calculus is used by the re-derivation.
|- (A.xph -> ph)
Theorem	ax467to6 1023	Re-derivation of ax-6o 976 from ax467 1021. Note that ax-6o 976 and ax-7 960 are not used by the re-derivation. The use of 19.20i 990 (which uses ax-4 971) is allowed since we have already proved ax467to4 1022.
|- (-. A.x -. A.xph -> ph)
Theorem	ax467to7 1024	Re-derivation of ax-7 960 from ax467 1021. Note that ax-6o 976 and ax-7 960 are not used by the re-derivation. The use of 19.20i 990 (which uses ax-4 971) is allowed since we have already proved ax467to4 1022.
|- (A.xA.yph -> A.yA.xph)
Theorem	modal-5 1025	The analog in our "pure" predicate calculus of axiom 5 of modal logic S5.
|- (-. A.x -. ph -> A.x -. A.x -. ph)
Theorem	modal-b 1026	The analog in our "pure" predicate calculus of the Brouwer axiom (B) of modal logic S5.
|- (ph -> A.x -. A.x -. ph)
Theorem	19.8a 1027	If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89.
|- (ph -> E.xph)
Theorem	19.2 1028	Theorem 19.2 of [Margaris] p. 89, generalized to use two set variables. (Contributed by O'Cat, 31-Mar-2008.)
|- (A.xph -> E.yph)
Theorem	19.3 1029	A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89.
|- (ph -> A.xph)   =>   |- (A.xph <-> ph)
Theorem	alcom 1030	Theorem 19.5 of [Margaris] p. 89.
|- (A.xA.yph <-> A.yA.xph)
Theorem	alnex 1031	Theorem 19.7 of [Margaris] p. 89.
|- (A.x -. ph <-> -. E.xph)
Theorem	alex 1032	Theorem 19.6 of [Margaris] p. 89.
|- (A.xph <-> -. E.x -. ph)
Theorem	19.9t 1033	A closed version of one direction of 19.9 1034.
|- (A.x(ph -> A.xph) -> (E.xph -> ph))
Theorem	19.9 1034	A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24-Mar-2007.)
|- (ph -> A.xph)   =>   |- (E.xph <-> ph)
Theorem	19.9d 1035	A deduction version of one direction of 19.9 1034.
|- (ps -> A.xps)   &   |- (ps -> (ph -> A.xph))   =>   |- (ps -> (E.xph -> ph))
Theorem	exnal 1036	Theorem 19.14 of [Margaris] p. 90.
|- (E.x -. ph <-> -. A.xph)
Theorem	19.22 1037	Theorem 19.22 of [Margaris] p. 90.
|- (A.x(ph -> ps) -> (E.xph -> E.xps))
Theorem	19.22i 1038	Inference adding existential quantifier to antecedent and consequent.
|- (ph -> ps)   =>   |- (E.xph -> E.xps)
Theorem	19.22i2 1039	Inference adding 2 existential quantifiers to antecedent and consequent.
|- (ph -> ps)   =>   |- (E.xE.yph -> E.xE.yps)
Theorem	alinexa 1040	A transformation of quantifiers and logical connectives.
|- (A.x(ph -> -. ps) <-> -. E.x(ph /\ ps))
Theorem	exanali 1041	A transformation of quantifiers and logical connectives.
|- (E.x(ph /\ -. ps) <-> -. A.x(ph -> ps))
Theorem	alexn 1042	A relationship between two quantifiers and negation.
|- (A.xE.y -. ph <-> -. E.xA.yph)
Theorem	excomim 1043	One direction of Theorem 19.11 of [Margaris] p. 89.
|- (E.xE.yph -> E.yE.xph)
Theorem	excom 1044	Theorem 19.11 of [Margaris] p. 89.
|- (E.xE.yph <-> E.yE.xph)
Theorem	19.12 1045	Theorem 19.12 of [Margaris] p. 89. Assuming the converse is a mistake sometimes made by beginners! But sometimes the converse does hold, as in 19.12vv 1300 and r19.12sn 2440.
|- (E.xA.yph -> A.yE.xph)
Theorem	19.16 1046	Theorem 19.16 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph <-> ps) -> (ph <-> A.xps))
Theorem	19.17 1047	Theorem 19.17 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph <-> ps) -> (A.xph <-> ps))
Theorem	19.18 1048	Theorem 19.18 of [Margaris] p. 90.
|- (A.x(ph <-> ps) -> (E.xph <-> E.xps))
Theorem	exbii 1049	Inference adding existential quantifier to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.xph <-> E.xps)
Theorem	2exbii 1050	Inference adding 2 existential quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.xE.yph <-> E.xE.yps)
Theorem	3exbi 1051	Inference adding 3 existential quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.xE.yE.zph <-> E.xE.yE.zps)
Theorem	exancom 1052	Commutation of conjunction inside an existential quantifier.
|- (E.x(ph /\ ps) <-> E.x(ps /\ ph))
Theorem	19.19 1053	Theorem 19.19 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph <-> ps) -> (ph <-> E.xps))
Theorem	19.21 1054	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "x is not free in ph."
|- (ph -> A.xph)   =>   |- (A.x(ph -> ps) <-> (ph -> A.xps))
Theorem	19.21-2 1055	Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers.
|- (ph -> A.xph)   &   |- (ph -> A.yph)   =>   |- (A.xA.y(ph -> ps) <-> (ph -> A.xA.yps))
Theorem	stdpc5 1056	An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis (ph -> A.xph) can be thought of as emulating "x is not free in ph." With this convention, the meaning of "not free" is less restrictive than the usual textbook definition; for example x would not (for us) be free in x = x by hbequid 1167. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5.
|- (ph -> A.xph)   =>   |- (A.x(ph -> ps) -> (ph -> A.xps))
Theorem	19.21ad 1057	Deduction from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ps -> A.xps)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> A.xch))
Theorem	19.21bi 1058	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> A.xps)   =>   |- (ph -> ps)
Theorem	19.21bbi 1059	Inference removing double quantifier.
|- (ph -> A.xA.yps)   =>   |- (ph -> ps)
Theorem	19.22d 1060	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> E.xch))
Theorem	19.23 1061	Theorem 19.23 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph -> ps) <-> (E.xph -> ps))
Theorem	19.23ai 1062	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (ps -> A.xps)   &   |- (ph -> ps)   =>   |- (E.xph -> ps)
Theorem	19.23bi 1063	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (E.xph -> ps)   =>   |- (ph -> ps)
Theorem	19.23ad 1064	Deduction from Theorem 19.23 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ch -> A.xch)   &