Metamath Proof Explorer - mmtheorems8

Jump to page: 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-5787

Statement List for Metamath Proof Explorer - 701-800 - Page 8 of 58

Type	Label	Description
Statement
Theorem	hbex 701	If x is not free in ph, it is not free in E.yph.
|- (ph -> A.xph)   =>   |- (E.yph -> A.xE.yph)
Theorem	hbim 702	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	hbor 703	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 704	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 705	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 706	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 707	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	hbn1 708	x is not free in -. A.xph.
|- (-. A.xph -> A.x -. A.xph)
Theorem	hbe1 709	x is not free in E.xph.
|- (E.xph -> A.xE.xph)
Theorem	hbnt 710	A closed form of hypothesis builder hbne 699.
|- (A.x(ph -> A.xph) -> (-. ph -> A.x -. ph))
Theorem	ax6 711	Axiom C5-2 of [Monk2] p. 113, which we prove from our ax-6 675 (and others). Conversely, ax-6 675 follows from this using ax-4 673 and propositional calculus, showing that they are interchangeable.
|- (-. A.xph -> A.x -. A.xph)
Theorem	19.8a 712	If a wff is true, it is true for at least one instance.
|- (ph -> E.xph)
Theorem	19.2 713	Theorem 19.2 of [Margaris] p. 89.
|- (A.xph -> E.xph)
Theorem	19.3r 714	A wff may be quantified with a variable not free in it.
|- (ph -> A.xph)   =>   |- (ph <-> A.xph)
Theorem	alcom 715	Theorem 19.5 of [Margaris] p. 89.
|- (A.xA.yph <-> A.yA.xph)
Theorem	alnex 716	Theorem 19.7 of [Margaris] p. 89.
|- (A.x -. ph <-> -. E.xph)
Theorem	alex 717	Theorem 19.6 of [Margaris] p. 89.
|- (A.xph <-> -. E.x -. ph)
Theorem	19.9r 718	Variation of Theorem 19.9 of [Margaris] p. 89.
|- (ph -> A.xph)   =>   |- (ph <-> E.xph)
Theorem	19.9t 719	A closed version of one direction of 19.9r 718.
|- (A.x(ph -> A.xph) -> (E.xph -> ph))
Theorem	19.9d 720	A deduction version of one direction of 19.9r 718.
|- (ps -> A.xps)   &   |- (ps -> (ph -> A.xph))   =>   |- (ps -> (E.xph -> ph))
Theorem	exnal 721	Theorem 19.14 of [Margaris] p. 90.
|- (E.x -. ph <-> -. A.xph)
Theorem	19.22 722	Theorem 19.22 of [Margaris] p. 90.
|- (A.x(ph -> ps) -> (E.xph -> E.xps))
Theorem	19.22i 723	Inference adding existential quantifier to antecedent and consequent.
|- (ph -> ps)   =>   |- (E.xph -> E.xps)
Theorem	alinexa 724	A transformation of quantifiers and logical connectives.
|- (A.x(ph -> -. ps) <-> -. E.x(ph /\ ps))
Theorem	exanali 725	A transformation of quantifiers and logical connectives.
|- (E.x(ph /\ -. ps) <-> -. A.x(ph -> ps))
Theorem	alexn 726	A relationship between two quantifiers and negation.
|- (A.xE.y -. ph <-> -. E.xA.yph)
Theorem	excomim 727	One direction of Theorem 19.11 of [Margaris] p. 89.
|- (E.xE.yph -> E.yE.xph)
Theorem	excom 728	Theorem 19.11 of [Margaris] p. 89.
|- (E.xE.yph <-> E.yE.xph)
Theorem	19.12 729	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 960.
|- (E.xA.yph -> A.yE.xph)
Theorem	19.16 730	Theorem 19.16 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph <-> ps) -> (ph <-> A.xps))
Theorem	19.17 731	Theorem 19.17 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph <-> ps) -> (A.xph <-> ps))
Theorem	19.18 732	Theorem 19.18 of [Margaris] p. 90.
|- (A.x(ph <-> ps) -> (E.xph <-> E.xps))
Theorem	biex 733	Inference adding existential quantifier to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.xph <-> E.xps)
Theorem	bi2ex 734	Inference adding 2 existential quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.xE.yph <-> E.xE.yps)
Theorem	bi3ex 735	Inference adding 3 existential quantifiers to both sides of an equivalence.
|- (ph <-> ps)   =>   |- (E.xE.yE.zph <-> E.xE.yE.zps)
Theorem	exancom 736	Commutation of conjunction inside an existential quantifier.
|- (E.x(ph /\ ps) <-> E.x(ps /\ ph))
Theorem	19.19 737	Theorem 19.19 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph <-> ps) -> (ph <-> E.xps))
Theorem	19.21 738	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	stdpc5 739	An axiom of standard predicate calculus. Axiom 5 of [Mendelson] p. 59. The hypothesis (ph -> A.xph) can be thought of as "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 since (by eqid 810 and hbth 697) we can prove (x = x -> A.xx = x).
|- (ph -> A.xph)   =>   |- (A.x(ph -> ps) -> (ph -> A.xps))
Theorem	19.21ai 740	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ph -> ps)   =>   |- (ph -> A.xps)
Theorem	19.21ad 741	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 742	Inference from Theorem 19.21 of [Margaris] p. 90.
|- (ph -> A.xps)   =>   |- (ph -> ps)
Theorem	19.21bbi 743	Inference removing double quantifier.
|- (ph -> A.xA.yps)   =>   |- (ph -> ps)
Theorem	19.22d 744	Deduction from Theorem 19.22 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> E.xch))
Theorem	19.23 745	Theorem 19.23 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph -> ps) <-> (E.xph -> ps))
Theorem	19.23ai 746	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (ps -> A.xps)   &   |- (ph -> ps)   =>   |- (E.xph -> ps)
Theorem	19.23bi 747	Inference from Theorem 19.23 of [Margaris] p. 90.
|- (E.xph -> ps)   =>   |- (ph -> ps)
Theorem	19.23ad 748	Deduction from Theorem 19.23 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- (ch -> A.xch)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (E.xps -> ch))
Theorem	19.26 749	Theorem 19.26 of [Margaris] p. 90.
|- (A.x(ph /\ ps) <-> (A.xph /\ A.xps))
Theorem	19.27 750	Theorem 19.27 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph /\ ps) <-> (A.xph /\ ps))
Theorem	19.28 751	Theorem 19.28 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph /\ ps) <-> (ph /\ A.xps))
Theorem	19.29 752	Theorem 19.29 of [Margaris] p. 90.
|- ((A.xph /\ E.xps) -> E.x(ph /\ ps))
Theorem	19.29r 753	Variation of Theorem 19.29 of [Margaris] p. 90.
|- ((E.xph /\ A.xps) -> E.x(ph /\ ps))
Theorem	19.35 754	Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier.
|- (E.x(ph -> ps) <-> (A.xph -> E.xps))
Theorem	19.35i 755	Inference from Theorem 19.35 of [Margaris] p. 90.
|- E.x(ph -> ps)   =>   |- (A.xph -> E.xps)
Theorem	19.35ri 756	Inference from Theorem 19.35 of [Margaris] p. 90.
|- (A.xph -> E.xps)   =>   |- E.x(ph -> ps)
Theorem	19.36 757	Theorem 19.36 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (E.x(ph -> ps) <-> (A.xph -> ps))
Theorem	19.36i 758	Inference from Theorem 19.36 of [Margaris] p. 90.
|- (ps -> A.xps)   &   |- E.x(ph -> ps)   =>   |- (A.xph -> ps)
Theorem	19.37 759	Theorem 19.37 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (E.x(ph -> ps) <-> (ph -> E.xps))
Theorem	19.38 760	Theorem 19.38 of [Margaris] p. 90.
|- ((E.xph -> A.xps) -> A.x(ph -> ps))
Theorem	19.39 761	Theorem 19.39 of [Margaris] p. 90.
|- ((E.xph -> E.xps) -> E.x(ph -> ps))
Theorem	19.24 762	Theorem 19.24 of [Margaris] p. 90.
|- ((A.xph -> A.xps) -> E.x(ph -> ps))
Theorem	19.25 763	Theorem 19.25 of [Margaris] p. 90.
|- (A.yE.x(ph -> ps) -> (E.yA.xph -> E.yE.xps))
Theorem	19.30 764	Theorem 19.30 of [Margaris] p. 90.
|- (A.x(ph \/ ps) -> (A.xph \/ E.xps))
Theorem	19.32 765	Theorem 19.32 of [Margaris] p. 90.
|- (ph -> A.xph)   =>   |- (A.x(ph \/ ps) <-> (ph \/ A.xps))
Theorem	19.31 766	Theorem 19.31 of [Margaris] p. 90.
|- (ps -> A.xps)   =>   |- (A.x(ph \/ ps) <-> (A.xph \/