mmtheorems4 - Metamath Proof Explorer

Home	Metamath Proof Explorer	< Previous Next >
		Browser slow? Try the Unicode version.

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-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17411

Color key:

Metamath Proof Explorer
(1-10419)

Hilbert Space Explorer
(10420-12013)

Users' Mathboxes
(12014-17411)

**Statement List for Metamath Proof Explorer -** 301-400 - Page 4 of 175
Type	Label	Description
Statement

Theorem	pm2.47 301	Theorem *2.47 of [WhiteheadRussell] p. 107.
$\/$ $\/$

Theorem	pm2.48 302	Theorem *2.48 of [WhiteheadRussell] p. 107.
$\/$ $\/$

Theorem	pm2.49 303	Theorem *2.49 of [WhiteheadRussell] p. 107.
$\/$ $\/$

Theorem	pm2.67 304	Theorem *2.67 of [WhiteheadRussell] p. 107.
$\/$

Theorem	pm3.2 305	Join antecedents with conjunction. Theorem *3.2 of [WhiteheadRussell] p. 111.
$/\$

Theorem	pm3.21 306	Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111.
$/\$

Theorem	pm3.2i 307	Infer conjunction of premises.
$/\$

Theorem	pm3.37 308	Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112.
$/\$ $/\$

Theorem	pm3.43i 309	Nested conjunction of antecedents.
$/\$

Theorem	jca 310	Deduce conjunction of the consequents of two implications ("join consequents with 'and'").
$/\$

Theorem	jca31 311	Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)
$/\$ $/\$

Theorem	jca32 312	Join three consequents. (Contributed by FL, 1-Aug-2009.)
$/\$ $/\$

Theorem	jcai 313	Deduction replacing implication with conjunction.
$/\$

Theorem	jctl 314	Inference conjoining a theorem to the left of a consequent.
$/\$

Theorem	jctr 315	Inference conjoining a theorem to the right of a consequent.
$/\$

Theorem	jctil 316	Inference conjoining a theorem to left of consequent in an implication.
$/\$

Theorem	jctir 317	Inference conjoining a theorem to right of consequent in an implication.
$/\$

Theorem	ancl 318	Conjoin antecedent to left of consequent.
$/\$

Theorem	ancr 319	Conjoin antecedent to right of consequent.
$/\$

Theorem	ancli 320	Deduction conjoining antecedent to left of consequent.
$/\$

Theorem	ancri 321	Deduction conjoining antecedent to right of consequent.
$/\$

Theorem	ancld 322	Deduction conjoining antecedent to left of consequent in nested implication.
$/\$

Theorem	ancrd 323	Deduction conjoining antecedent to right of consequent in nested implication.
$/\$

Theorem	anc2l 324	Conjoin antecedent to left of consequent in nested implication.
$/\$

Theorem	anc2r 325	Conjoin antecedent to right of consequent in nested implication.
$/\$

Theorem	anc2li 326	Deduction conjoining antecedent to left of consequent in nested implication.
$/\$

Theorem	anc2ri 327	Deduction conjoining antecedent to right of consequent in nested implication.
$/\$

Theorem	anor 328	Conjunction in terms of disjunction (DeMorgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120.
$/\$ $\/$

Theorem	ianor 329	Negated conjunction in terms of disjunction (DeMorgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (The proof was shortened by Andrew Salmon, 13-May-2011.)
$/\$ $\/$

Theorem	ianorOLD 330	Negated conjunction in terms of disjunction (DeMorgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120.
$/\$ $\/$

Theorem	ioran 331	Negated disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (The proof was shortened by Andrew Salmon, 7-May-2011.)
$\/$ $/\$

Theorem	ioranOLD 332	Negated disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120.
$\/$ $/\$

Theorem	pm4.52 333	Theorem *4.52 of [WhiteheadRussell] p. 120.
$/\$ $\/$

Theorem	pm4.53 334	Theorem *4.53 of [WhiteheadRussell] p. 120.
$/\$ $\/$

Theorem	pm4.54 335	Theorem *4.54 of [WhiteheadRussell] p. 120.
$/\$ $\/$

Theorem	pm4.55 336	Theorem *4.55 of [WhiteheadRussell] p. 120.
$/\$ $\/$

Theorem	pm4.56 337	Theorem *4.56 of [WhiteheadRussell] p. 120.
$/\$ $\/$

Theorem	oran 338	Disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (The proof was shortened by Andrew Salmon, 7-May-2011.)
$\/$ $/\$

Theorem	oranOLD 339	Disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.57 of [WhiteheadRussell] p. 120.
$\/$ $/\$

Theorem	pm4.57 340	Theorem *4.57 of [WhiteheadRussell] p. 120.
$/\$ $\/$

Theorem	pm3.1 341	Theorem *3.1 of [WhiteheadRussell] p. 111.
$/\$ $\/$

Theorem	pm3.11 342	Theorem *3.11 of [WhiteheadRussell] p. 111.
$\/$ $/\$

Theorem	pm3.12 343	Theorem *3.12 of [WhiteheadRussell] p. 111.
$\/$ $\/$ $/\$

Theorem	pm3.13 344	Theorem *3.13 of [WhiteheadRussell] p. 111.
$/\$ $\/$

Theorem	pm3.14 345	Theorem *3.14 of [WhiteheadRussell] p. 111.
$\/$ $/\$

Theorem	simpl 346	Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112.
$/\$

Theorem	simpli 347	Inference eliminating a conjunct.
$/\$

Theorem	simplld 348	Deduction eliminating a conjunct.
$/\$

Theorem	simplbi 349	Deduction eliminating a conjunct.
$/\$

Theorem	simpr 350	Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112.
$/\$

Theorem	simpri 351	Inference eliminating a conjunct.
$/\$

Theorem	simprd 352	Deduction eliminating a conjunct.
$/\$

Theorem	simprbi 353	Deduction eliminating a conjunct.
$/\$

Theorem	pm3.41 354	Theorem *3.41 of [WhiteheadRussell] p. 113.
$/\$

Theorem	pm3.42 355	Theorem *3.42 of [WhiteheadRussell] p. 113.
$/\$

Theorem	anclb 356	Conjoin antecedent to left of consequent. Theorem *4.7 of [WhiteheadRussell] p. 120.
$/\$

Theorem	ancrb 357	Conjoin antecedent to right of consequent.
$/\$

Theorem	pm3.4 358	Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113.
$/\$

Theorem	pm4.45im 359	Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119.
$/\$

Theorem	anim12i 360	Conjoin antecedents and consequents of two premises.
$/\$ $/\$

Theorem	anim1i 361	Introduce conjunct to both sides of an implication.
$/\$ $/\$

Theorem	anim2i 362	Introduce conjunct to both sides of an implication.
$/\$ $/\$

Theorem	orim12i 363	Disjoin antecedents and consequents of two premises.
$\/$ $\/$

Theorem	orim1i 364	Introduce disjunct to both sides of an implication.
$\/$ $\/$

Theorem	orim2i 365	Introduce disjunct to both sides of an implication.
$\/$ $\/$

Theorem	pm2.3 366	Theorem *2.3 of [WhiteheadRussell] p. 104.
$\/$ $\/$ $\/$ $\/$

Theorem	jao 367	Disjunction of antecedents. Compare Theorem *3.44 of [WhiteheadRussell] p. 113.
$\/$

Theorem	jaoi 368	Inference disjoining the antecedents of two implications.
$\/$

Theorem	pm2.41 369	Theorem *2.41 of [WhiteheadRussell] p. 106.
$\/$ $\/$ $\/$

Theorem	pm2.42 370	Theorem *2.42 of [WhiteheadRussell] p. 106.
$\/$

Theorem	pm2.4 371	Theorem *2.4 of [WhiteheadRussell] p. 106.
$\/$ $\/$ $\/$

Theorem	pm4.44 372	Theorem *4.44 of [WhiteheadRussell] p. 119.
$\/$ $/\$

Theorem	pm5.63 373	Theorem *5.63 of [WhiteheadRussell] p. 125.
$\/$ $\/$ $/\$

Theorem	impexp 374	Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122.
$/\$

Theorem	pm3.3 375	Theorem *3.3 (Exp) of [WhiteheadRussell] p. 112.
$/\$

Theorem	pm3.31 376	Theorem *3.31 (Imp) of [WhiteheadRussell] p. 112.
$/\$

Theorem	imp 377	Importation inference. (The proof was shortened by Eric Schmidt, 22-Dec-2006.)
$/\$

Theorem	impcom 378	Importation inference with commuted antecedents.
$/\$

Theorem	pm4.14 379	Theorem *4.14 of [WhiteheadRussell] p. 117.
$/\$ $/\$

Theorem	pm4.15 380	Theorem *4.15 of [WhiteheadRussell] p. 117.
$/\$ $/\$

Theorem	pm4.78 381	Theorem *4.78 of [WhiteheadRussell] p. 121.
$\/$ $\/$

Theorem	pm4.79 382	Theorem *4.79 of [WhiteheadRussell] p. 121.
$\/$ $/\$

Theorem	pm4.87 383	Theorem *4.87 of [WhiteheadRussell] p. 122. (The proof was shortened by Eric Schmidt, 26-Oct-2006.)
$/\$ $/\$ $/\$ $/\$

Theorem	pm3.33 384	Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112.
$/\$

Theorem	pm3.34 385	Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112.
$/\$

Theorem	pm3.35 386	Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112.
$/\$

Theorem	pm5.31 387	Theorem *5.31 of [WhiteheadRussell] p. 125.
$/\$ $/\$

Theorem	imp3a 388	Importation deduction.
$/\$

Theorem	imp31 389	An importation inference.
$/\$ $/\$

Theorem	imp32 390	An importation inference.
$/\$ $/\$

Theorem	imp4a 391	An importation inference.
$/\$

Theorem	imp4b 392	An importation inference.
$/\$ $/\$

Theorem	imp4c 393	An importation inference.
$/\$ $/\$

Theorem	imp4d 394	An importation inference.
$/\$ $/\$

Theorem	imp41 395	An importation inference.
$/\$ $/\$ $/\$

Theorem	imp42 396	An importation inference.
$/\$ $/\$ $/\$

Theorem	imp43 397	An importation inference.
$/\$ $/\$ $/\$

Theorem	imp44 398	An importation inference.
$/\$ $/\$ $/\$

Theorem	imp45 399	An importation inference.
$/\$ $/\$ $/\$

Theorem	imp5a 400	An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.)
$/\$

MPE Home Contents

< Previous Next >