mmtheorems18 - 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-10684

Statement List for Metamath Proof Explorer - 1701-1800 - Page 18 of 107

Type	Label	Description
Statement
Theorem	r19.20i 1701	Inference quantifying both antecedent and consequent.
|- (x e. A -> (ph -> ps))   =>   |- (A.x e. A ph -> A.x e. A ps)
Theorem	r19.20ia 1702	Inference quantifying both antecedent and consequent.
|- ((x e. A /\ ph) -> ps)   =>   |- (A.x e. A ph -> A.x e. A ps)
Theorem	r19.20si 1703	Inference quantifying both antecedent and consequent, with strong hypothesis.
|- (ph -> ps)   =>   |- (A.x e. A ph -> A.x e. A ps)
Theorem	r19.20sii 1704	Inference quantifying antecedent, nested antecedent, and consequent, with a strong hypothesis.
|- (ph -> (ps -> ch))   =>   |- (A.x e. A ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	r19.20da 1705	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90.
|- (ph -> A.xph)   &   |- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	r19.20dva 1706	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90.
|- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	r19.20sdv 1707	Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90.
|- (ph -> (ps -> ch))   =>   |- (ph -> (A.x e. A ps -> A.x e. A ch))
Theorem	r19.20dv2 1708	Inference quantifying both antecedent and consequent.
|- (ph -> ((x e. A -> ps) -> (x e. B -> ch)))   =>   |- (ph -> (A.x e. A ps -> A.x e. B ch))
Theorem	r19.21ai 1709	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> A.xph)   &   |- (ph -> (x e. A -> ps))   =>   |- (ph -> A.x e. A ps)
Theorem	r19.21aiv 1710	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> (x e. A -> ps))   =>   |- (ph -> A.x e. A ps)
Theorem	r19.21aiva 1711	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- ((ph /\ x e. A) -> ps)   =>   |- (ph -> A.x e. A ps)
Theorem	r19.21t 1712	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers (closed theorem version).
|- (A.x(ph -> A.xph) -> (A.x e. A (ph -> ps) <-> (ph -> A.x e. A ps)))
Theorem	r19.21v 1713	Theorem 19.21 of [Margaris] p. 90 with restricted quantifiers.
|- (A.x e. A (ph -> ps) <-> (ph -> A.x e. A ps))
Theorem	r19.21ad 1714	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> A.xph)   &   |- (ps -> A.xps)   &   |- (ph -> (ps -> (x e. A -> ch)))   =>   |- (ph -> (ps -> A.x e. A ch))
Theorem	r19.21adv 1715	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> (ps -> (x e. A -> ch)))   =>   |- (ph -> (ps -> A.x e. A ch))
Theorem	r19.21adva 1716	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (ps -> A.x e. A ch))
Theorem	r19.21aivv 1717	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.)
|- (ph -> ((x e. A /\ y e. B) -> ps))   =>   |- (ph -> A.x e. A A.y e. B ps)
Theorem	r19.21advv 1718	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.)
|- (ph -> (ps -> ((x e. A /\ y e. B) -> ch)))   =>   |- (ph -> (ps -> A.x e. A A.y e. B ch))
Theorem	r19.21advva 1719	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.)
|- ((ph /\ (x e. A /\ y e. B)) -> (ps -> ch))   =>   |- (ph -> (ps -> A.x e. A A.y e. B ch))
Theorem	rgen2 1720	Generalization rule for restricted quantification.
|- ((x e. A /\ y e. B) -> ph)   =>   |- A.x e. A A.y e. B ph
Theorem	rgen3 1721	Generalization rule for restricted quantification.
|- ((x e. A /\ y e. B /\ z e. C) -> ph)   =>   |- A.x e. A A.y e. B A.z e. C ph
Theorem	r19.21bi 1722	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> A.x e. A ps)   =>   |- ((ph /\ x e. A) -> ps)
Theorem	rspec2 1723	Specialization rule for restricted quantification.
|- A.x e. A A.y e. B ph   =>   |- ((x e. A /\ y e. B) -> ph)
Theorem	rspec3 1724	Specialization rule for restricted quantification.
|- A.x e. A A.y e. B A.z e. C ph   =>   |- ((x e. A /\ y e. B /\ z e. C) -> ph)
Theorem	r19.21be 1725	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> A.x e. A ps)   =>   |- A.x e. A (ph -> ps)
Theorem	nrex 1726	Inference adding restricted existential quantifier to negated wff.
|- (x e. A -> -. ps)   =>   |- -. E.x e. A ps
Theorem	nrexdv 1727	Deduction adding restricted existential quantifier to negated wff.
|- ((ph /\ x e. A) -> -. ps)   =>   |- (ph -> -. E.x e. A ps)
Theorem	r19.22 1728	Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.)
|- (A.x e. A (ph -> ps) -> (E.x e. A ph -> E.x e. A ps))
Theorem	r19.22i 1729	Inference quantifying both antecedent and consequent.
|- (x e. A -> (ph -> ps))   =>   |- (E.x e. A ph -> E.x e. A ps)
Theorem	r19.22i2 1730	Inference quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
|- ((x e. A /\ ph) -> (x e. B /\ ps))   =>   |- (E.x e. A ph -> E.x e. B ps)
Theorem	r19.22si 1731	Inference quantifying both antecedent and consequent.
|- (ph -> ps)   =>   |- (E.x e. A ph -> E.x e. A ps)
Theorem	r19.22d 1732	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> A.xph)   &   |- (ph -> (x e. A -> (ps -> ch)))   =>   |- (ph -> (E.x e. A ps -> E.x e. A ch))
Theorem	r19.22dv2 1733	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
|- (ph -> ((x e. A /\ ps) -> (x e. B /\ ch)))   =>   |- (ph -> (E.x e. A ps -> E.x e. B ch))
Theorem	r19.22dv 1734	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
|- (ph -> (x e. A -> (ps -> ch)))   =>   |- (ph -> (E.x e. A ps -> E.x e. A ch))
Theorem	r19.22sdv 1735	Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.)
|- (ph -> (ps -> ch))   =>   |- (ph -> (E.x e. A ps -> E.x e. A ch))
Theorem	r19.22dva 1736	Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.
|- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (E.x e. A ps -> E.x e. A ch))
Theorem	r19.12 1737	Theorem 19.12 of [Margaris] p. 89 with restricted quantifiers.
|- (E.x e. A A.y e. B ph -> A.y e. B E.x e. A ph)
Theorem	r19.23v 1738	Theorem 19.23 of [Margaris] p. 90 with restricted quantifiers.
|- (A.x e. A (ph -> ps) <-> (E.x e. A ph -> ps))
Theorem	r19.23ai 1739	Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ps -> A.xps)   &   |- (x e. A -> (ph -> ps))   =>   |- (E.x e. A ph -> ps)
Theorem	r19.23aiv 1740	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.)
|- (x e. A -> (ph -> ps))   =>   |- (E.x e. A ph -> ps)
Theorem	r19.23aiva 1741	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).
|- ((x e. A /\ ph) -> ps)   =>   |- (E.x e. A ph -> ps)
Theorem	r19.23ad 1742	Deduction from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).
|- (ph -> A.xph)   &   |- (ch -> A.xch)   &   |- (ph -> (x e. A -> (ps -> ch)))   =>   |- (ph -> (E.x e. A ps -> ch))
Theorem	r19.23adv 1743	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (The proof was shortened by Eric Schmidt, 22-Dec-2006.)
|- (ph -> (x e. A -> (ps -> ch)))   =>   |- (ph -> (E.x e. A ps -> ch))
Theorem	r19.23adva 1744	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).
|- ((ph /\ x e. A) -> (ps -> ch))   =>   |- (ph -> (E.x e. A ps -> ch))
Theorem	r19.23aivv 1745	Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).
|- ((x e. A /\ y e. B) -> (ph -> ps))   =>   |- (E.x e. A E.y e. B ph -> ps)
Theorem	r19.23advv 1746	Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.)
|- (ph -> ((x e. A /\ y e. B) -> (ps -> ch)))   =>   |- (ph -> (E.x e. A E.y e. B ps -> ch))
Theorem	r19.26 1747	Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers.
|- (A.x e. A (ph /\ ps) <-> (A.x e. A ph /\ A.x e. A ps))
Theorem	r19.26-2 1748	Theorem 19.26 of [Margaris] p. 90 with 2 restricted quantifiers.
|- (A.x e. A A.y e. B (ph /\ ps) <-> (A.x e. A A.y e. B ph /\ A.x e. A A.y e. B ps))
Theorem	r19.26m 1749	Theorem 19.26 of [Margaris] p. 90 with mixed quantifiers.
|- (A.x((x e. A -> ph) /\ (x e. B -> ps)) <-> (A.x e. A ph /\ A.x e. B ps))
Theorem	r19.15 1750	Distribute a restricted universal quantifier over a biconditional. Theorem 19.15 of [Margaris] p. 90 with restricted quantification.
|- (A.x e. A (ph <-> ps) -> (A.x e. A ph <-> A.x e. A ps))
Theorem	r19.27av 1751	Restricted version of one direction of Theorem 19.27 of [Margaris] p. 90. (The other direction doesn't hold when A is empty.)
|- ((A.x e. A ph /\ ps) ->