mmtheorems4 - 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-10674

Statement List for Metamath Proof Explorer - 301-400 - Page 4 of 107

Type	Label	Description
Statement
Theorem	anc2r 301	Conjoin antecedent to right of consequent in nested implication.
|- ((ph -> (ps -> ch)) -> (ph -> (ps -> (ch /\ ph))))
Theorem	anc2li 302	Deduction conjoining antecedent to left of consequent in nested implication.
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> (ph /\ ch)))
Theorem	anc2ri 303	Deduction conjoining antecedent to right of consequent in nested implication.
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> (ch /\ ph)))
Theorem	anor 304	Conjunction in terms of disjunction (DeMorgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120.
|- ((ph /\ ps) <-> -. (-. ph \/ -. ps))
Theorem	ianor 305	Negated conjunction in terms of disjunction (DeMorgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120.
|- (-. (ph /\ ps) <-> (-. ph \/ -. ps))
Theorem	ioran 306	Negated disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120.
|- (-. (ph \/ ps) <-> (-. ph /\ -. ps))
Theorem	pm4.52 307	Theorem *4.52 of [WhiteheadRussell] p. 120.
|- ((ph /\ -. ps) <-> -. (-. ph \/ ps))
Theorem	pm4.53 308	Theorem *4.53 of [WhiteheadRussell] p. 120.
|- (-. (ph /\ -. ps) <-> (-. ph \/ ps))
Theorem	pm4.54 309	Theorem *4.54 of [WhiteheadRussell] p. 120.
|- ((-. ph /\ ps) <-> -. (ph \/ -. ps))
Theorem	pm4.55 310	Theorem *4.55 of [WhiteheadRussell] p. 120.
|- (-. (-. ph /\ ps) <-> (ph \/ -. ps))
Theorem	pm4.56 311	Theorem *4.56 of [WhiteheadRussell] p. 120.
|- ((-. ph /\ -. ps) <-> -. (ph \/ ps))
Theorem	oran 312	Disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.57 of [WhiteheadRussell] p. 120.
|- ((ph \/ ps) <-> -. (-. ph /\ -. ps))
Theorem	pm4.57 313	Theorem *4.57 of [WhiteheadRussell] p. 120.
|- (-. (-. ph /\ -. ps) <-> (ph \/ ps))
Theorem	pm3.1 314	Theorem *3.1 of [WhiteheadRussell] p. 111.
|- ((ph /\ ps) -> -. (-. ph \/ -. ps))
Theorem	pm3.11 315	Theorem *3.11 of [WhiteheadRussell] p. 111.
|- (-. (-. ph \/ -. ps) -> (ph /\ ps))
Theorem	pm3.12 316	Theorem *3.12 of [WhiteheadRussell] p. 111.
|- ((-. ph \/ -. ps) \/ (ph /\ ps))
Theorem	pm3.13 317	Theorem *3.13 of [WhiteheadRussell] p. 111.
|- (-. (ph /\ ps) -> (-. ph \/ -. ps))
Theorem	pm3.14 318	Theorem *3.14 of [WhiteheadRussell] p. 111.
|- ((-. ph \/ -. ps) -> -. (ph /\ ps))
Theorem	pm3.26 319	Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112.
|- ((ph /\ ps) -> ph)
Theorem	pm3.26i 320	Inference eliminating a conjunct.
|- (ph /\ ps)   =>   |- ph
Theorem	pm3.26d 321	Deduction eliminating a conjunct.
|- (ph -> (ps /\ ch))   =>   |- (ph -> ps)
Theorem	pm3.26bi 322	Deduction eliminating a conjunct.
|- (ph <-> (ps /\ ch))   =>   |- (ph -> ps)
Theorem	pm3.27 323	Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112.
|- ((ph /\ ps) -> ps)
Theorem	pm3.27i 324	Inference eliminating a conjunct.
|- (ph /\ ps)   =>   |- ps
Theorem	pm3.27d 325	Deduction eliminating a conjunct.
|- (ph -> (ps /\ ch))   =>   |- (ph -> ch)
Theorem	pm3.27bi 326	Deduction eliminating a conjunct.
|- (ph <-> (ps /\ ch))   =>   |- (ph -> ch)
Theorem	pm3.41 327	Theorem *3.41 of [WhiteheadRussell] p. 113.
|- ((ph -> ch) -> ((ph /\ ps) -> ch))
Theorem	pm3.42 328	Theorem *3.42 of [WhiteheadRussell] p. 113.
|- ((ps -> ch) -> ((ph /\ ps) -> ch))
Theorem	anclb 329	Conjoin antecedent to left of consequent. Theorem *4.7 of [WhiteheadRussell] p. 120.
|- ((ph -> ps) <-> (ph -> (ph /\ ps)))
Theorem	ancrb 330	Conjoin antecedent to right of consequent.
|- ((ph -> ps) <-> (ph -> (ps /\ ph)))
Theorem	pm3.4 331	Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113.
|- ((ph /\ ps) -> (ph -> ps))
Theorem	pm4.45im 332	Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119.
|- (ph <-> (ph /\ (ps -> ph)))
Theorem	anim12i 333	Conjoin antecedents and consequents of two premises.
|- (ph -> ps)   &   |- (ch -> th)   =>   |- ((ph /\ ch) -> (ps /\ th))
Theorem	anim1i 334	Introduce conjunct to both sides of an implication.
|- (ph -> ps)   =>   |- ((ph /\ ch) -> (ps /\ ch))
Theorem	anim2i 335	Introduce conjunct to both sides of an implication.
|- (ph -> ps)   =>   |- ((ch /\ ph) -> (ch /\ ps))
Theorem	orim12i 336	Disjoin antecedents and consequents of two premises.
|- (ph -> ps)   &   |- (ch -> th)   =>   |- ((ph \/ ch) -> (ps \/ th))
Theorem	orim1i 337	Introduce disjunct to both sides of an implication.
|- (ph -> ps)   =>   |- ((ph \/ ch) -> (ps \/ ch))
Theorem	orim2i 338	Introduce disjunct to both sides of an implication.
|- (ph -> ps)   =>   |- ((ch \/ ph) -> (ch \/ ps))
Theorem	pm2.3 339	Theorem *2.3 of [WhiteheadRussell] p. 104.
|- ((ph \/ (ps \/ ch)) -> (ph \/ (ch \/ ps)))
Theorem	jao 340	Disjunction of antecedents. Compare Theorem *3.44 of [WhiteheadRussell] p. 113.
|- ((ph -> ps) -> ((ch -> ps) -> ((ph \/ ch) -> ps)))
Theorem	jaoi 341	Inference disjoining the antecedents of two implications.
|- (ph -> ps)   &   |- (ch -> ps)   =>   |- ((ph \/ ch) -> ps)
Theorem	pm2.41 342	Theorem *2.41 of [WhiteheadRussell] p. 106.
|- ((ps \/ (ph \/ ps)) -> (ph \/ ps))
Theorem	pm2.42 343	Theorem *2.42 of [WhiteheadRussell] p. 106.
|- ((-. ph \/ (ph -> ps)) -> (ph -> ps))
Theorem	pm2.4 344	Theorem *2.4 of [WhiteheadRussell] p. 106.
|- ((ph \/ (ph \/ ps)) -> (ph \/ ps))
Theorem	pm4.44 345	Theorem *4.44 of [WhiteheadRussell] p. 119.
|- (ph <-> (ph \/ (ph /\ ps)))
Theorem	pm5.63 346	Theorem *5.63 of [WhiteheadRussell] p. 125.
|- ((ph \/ ps) <-> (ph \/ (-. ph /\ ps)))
Theorem	impexp 347	Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122.
|- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))
Theorem	pm3.3 348	Theorem *3.3 (Exp) of [WhiteheadRussell] p. 112.
|- (((ph /\ ps) -> ch) -> (ph -> (ps -> ch)))
Theorem	pm3.31 349	Theorem *3.31 (Imp) of [WhiteheadRussell] p. 112.
|- ((ph -> (ps -> ch)) -> ((ph /\ ps) -> ch))
Theorem	imp 350	Importation inference. (The proof was shortened by Eric Schmidt, 22-Dec-2006.)
|- (ph -> (ps -> ch))   =>   |- ((ph /\ ps) -> ch)
Theorem	impcom 351	Importation inference with commuted antecedents.
|- (ph -> (ps -> ch))   =>   |- ((ps /\ ph) -> ch)
Theorem	pm4.14 352	Theorem *4.14 of [WhiteheadRussell] p. 117.
|- (((ph /\ ps) -> ch) <-> ((ph /\ -. ch) -> -. ps))
Theorem	pm4.15 353	Theorem *4.15 of [WhiteheadRussell] p. 117.
|- (((ph /\ ps) -> -. ch) <-> ((ps /\ ch) -> -. ph))
Theorem	pm4.78 354	Theorem *4.78 of [WhiteheadRussell] p. 121.
|- (((ph -> ps) \/ (ph -> ch)) <-> (ph -> (ps \/ ch)))
Theorem	pm4.79 355	Theorem *4.79 of [WhiteheadRussell] p. 121.
|- (((ps -> ph) \/ (ch -> ph)) <-> ((ps /\ ch) -> ph))
Theorem	pm4.87 356	Theorem *4.87 of [WhiteheadRussell] p. 122. (The proof was shortened by Eric Schmidt, 26-Oct-2006.)
|- (((((ph /\ ps) -> ch) <-> (ph -> (ps -> ch))) /\ ((ph -> (ps -> ch)) <-> (ps -> (ph -> ch)))) /\ ((ps -> (ph -> ch)) <-> ((ps /\ ph) -> ch)))
Theorem	pm3.33 357	Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112.
|- (((ph -> ps) /\ (ps -> ch)) -> (ph -> ch))
Theorem	pm3.34 358	Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112.
|- (((ps -> ch) /\ (ph -> ps)) -> (ph -> ch))
Theorem	pm3.35 359	Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112.
|- ((ph /\ (ph -> ps)) -> ps)
Theorem	pm5.31 360	Theorem *5.31 of [WhiteheadRussell] p. 125.
|- ((ch /\ (ph -> ps)) -> (ph -> (ps /\ ch)))
Theorem	imp3a 361	Importation deduction.
|- (ph -> (ps -> (ch -> th)))   =>   |- (ph -> ((ps /\ ch) -> th))
Theorem	imp31 362	An importation inference.
|- (ph -> (ps -> (ch -> th)))   =>   |- (((ph /\ ps) /\ ch) -> th)
Theorem	imp32 363	An importation inference.
|- (ph -> (ps -> (ch -> th)))   =>   |- ((ph /\ (ps /\ ch)) -> th)
Theorem	imp4a 364	An importation inference.
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (ph -> (ps -> ((ch /\ th) -> ta)))
Theorem	imp4b 365	An importation inference.
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- ((ph /\ ps) -> ((ch /\ th) -> ta))
Theorem	imp4c 366	An importation inference.
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (ph -> (((ps /\ ch) /\ th) -> ta))
Theorem	imp4d 367	An importation inference.
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- (ph -> ((ps /\ (ch /\ th)) -> ta))
Theorem	imp41 368	An importation inference.
|- (ph -> (ps -> (ch -> (th -> ta))))   =>   |- ((((ph /\ ps) /\ ch) /\ th) -> ta)
Theorem	imp42 369	An importation inference.
|- (ph -> (ps -> (ch -> (th -> ta))))   =>