Metamath Proof Explorer - mmtheorems3

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 - 201-300 - Page 3 of 58

Type	Label	Description
Statement
Theorem	orri 201	Inference from disjunction definition.
|- (-. ph -> ps)   =>   |- (ph \/ ps)
Theorem	ord 202	Deduction from disjunction definition.
|- (ph -> (ps \/ ch))   =>   |- (ph -> (-. ps -> ch))
Theorem	orrd 203	Deduction from disjunction definition.
|- (ph -> (-. ps -> ch))   =>   |- (ph -> (ps \/ ch))
Theorem	imor 204	Implication in terms of disjunction. Theorem *4.6 of [WhiteheadRussell] p. 120.
|- ((ph -> ps) <-> (-. ph \/ ps))
Theorem	iman 205	Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176.
|- ((ph -> ps) <-> -. (ph /\ -. ps))
Theorem	annim 206	Express conjunction in terms of implication.
|- ((ph /\ -. ps) <-> -. (ph -> ps))
Theorem	imnan 207	Express implication in terms of conjunction.
|- ((ph -> -. ps) <-> -. (ph /\ ps))
Theorem	oridm 208	Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117.
|- ((ph \/ ph) <-> ph)
Theorem	orcom 209	Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118.
|- ((ph \/ ps) <-> (ps \/ ph))
Theorem	pm2.62 210	Theorem *2.62 of [WhiteheadRussell] p. 107.
|- ((ph \/ ps) -> ((ph -> ps) -> ps))
Theorem	pm2.621 211	Theorem *2.621 of [WhiteheadRussell] p. 107.
|- ((ph -> ps) -> ((ph \/ ps) -> ps))
Theorem	orel1 212	Elimination of disjunction by denial of a disjunct. Theorem *2.55 of [WhiteheadRussell] p. 107.
|- (-. ph -> ((ph \/ ps) -> ps))
Theorem	orel2 213	Elimination of disjunction by denial of a disjunct. Theorem *2.56 of [WhiteheadRussell] p. 107.
|- (-. ph -> ((ps \/ ph) -> ps))
Theorem	orbi2i 214	Inference adding a left disjunct to both sides of a logical equivalence.
|- (ph <-> ps)   =>   |- ((ch \/ ph) <-> (ch \/ ps))
Theorem	orbi1i 215	Inference adding a right disjunct to both sides of a logical equivalence.
|- (ph <-> ps)   =>   |- ((ph \/ ch) <-> (ps \/ ch))
Theorem	orbi12i 216	Infer the disjunction of two equivalences.
|- (ph <-> ps)   &   |- (ch <-> th)   =>   |- ((ph \/ ch) <-> (ps \/ th))
Theorem	or12 217	A rearrangement of disjuncts.
|- ((ph \/ (ps \/ ch)) <-> (ps \/ (ph \/ ch)))
Theorem	orass 218	Associative law for disjunction. Theorem *4.33 of [WhiteheadRussell] p. 118.
|- (((ph \/ ps) \/ ch) <-> (ph \/ (ps \/ ch)))
Theorem	or23 219	A rearrangement of disjuncts.
|- (((ph \/ ps) \/ ch) <-> ((ph \/ ch) \/ ps))
Theorem	or4 220	Rearrangement of 4 disjuncts.
|- (((ph \/ ps) \/ (ch \/ th)) <-> ((ph \/ ch) \/ (ps \/ th)))
Theorem	or42 221	Rearrangement of 4 disjuncts.
|- (((ph \/ ps) \/ (ch \/ th)) <-> ((ph \/ ch) \/ (th \/ ps)))
Theorem	orordi 222	Distribution of disjunction over disjunction.
|- ((ph \/ (ps \/ ch)) <-> ((ph \/ ps) \/ (ph \/ ch)))
Theorem	orordir 223	Distribution of disjunction over disjunction.
|- (((ph \/ ps) \/ ch) <-> ((ph \/ ch) \/ (ps \/ ch)))
Theorem	olc 224	Introduction of a disjunct. Axiom *1.3 of [WhiteheadRussell] p. 96.
|- (ph -> (ps \/ ph))
Theorem	orc 225	Introduction of a disjunct. Theorem *2.2 of [WhiteheadRussell] p. 104.
|- (ph -> (ph \/ ps))
Theorem	orci 226	Deduction eliminating disjunct.
|- ((ph \/ ps) -> ch)   =>   |- (ph -> ch)
Theorem	olci 227	Deduction eliminating disjunct.
|- ((ph \/ ps) -> ch)   =>   |- (ps -> ch)
Theorem	pm2.45 228	Theorem *2.45 of [WhiteheadRussell] p. 106.
|- (-. (ph \/ ps) -> -. ph)
Theorem	pm2.46 229	Theorem *2.46 of [WhiteheadRussell] p. 106.
|- (-. (ph \/ ps) -> -. ps)
Theorem	pm2.48 230	Theorem *2.48 of [WhiteheadRussell] p. 107.
|- (-. (ph \/ ps) -> (ph \/ -. ps))
Theorem	pm2.67 231	Theorem *2.67 of [WhiteheadRussell] p. 107.
|- (((ph \/ ps) -> ps) -> (ph -> ps))
Theorem	pm3.2 232	Join antecedents with conjunction. Theorem *3.2 of [WhiteheadRussell] p. 111.
|- (ph -> (ps -> (ph /\ ps)))
Theorem	pm3.21 233	Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111.
|- (ph -> (ps -> (ps /\ ph)))
Theorem	pm3.2i 234	Infer conjunction of premises.
|- ph   &   |- ps   =>   |- (ph /\ ps)
Theorem	pm3.43i 235	Nested conjunction of antecedents.
|- ((ph -> ps) -> ((ph -> ch) -> (ph -> (ps /\ ch))))
Theorem	jca 236	Deduce conjunction of the consequents of two implications ("join consequents with 'and'").
|- (ph -> ps)   &   |- (ph -> ch)   =>   |- (ph -> (ps /\ ch))
Theorem	jcai 237	Deduction replacing implication with conjunction.
|- (ph -> ps)   &   |- (ph -> (ps -> ch))   =>   |- (ph -> (ps /\ ch))
Theorem	jctl 238	Inference conjoining a theorem to the left of a consequent.
|- ps   =>   |- (ph -> (ps /\ ph))
Theorem	jctr 239	Inference conjoining a theorem to the right of a consequent.
|- ps   =>   |- (ph -> (ph /\ ps))
Theorem	jctil 240	Inference conjoining a theorem to left of consequent in an implication.
|- (ph -> ps)   &   |- ch   =>   |- (ph -> (ch /\ ps))
Theorem	jctir 241	Inference conjoining a theorem to right of consequent in an implication.
|- (ph -> ps)   &   |- ch   =>   |- (ph -> (ps /\ ch))
Theorem	ancl 242	Conjoin antecedent to left of consequent.
|- ((ph -> ps) -> (ph -> (ph /\ ps)))
Theorem	ancr 243	Conjoin antecedent to right of consequent.
|- ((ph -> ps) -> (ph -> (ps /\ ph)))
Theorem	ancli 244	Deduction conjoining antecedent to left of consequent.
|- (ph -> ps)   =>   |- (ph -> (ph /\ ps))
Theorem	ancri 245	Deduction conjoining antecedent to right of consequent.
|- (ph -> ps)   =>   |- (ph -> (ps /\ ph))
Theorem	ancld 246	Deduction conjoining antecedent to left of consequent in nested implication.
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> (ps /\ ch)))
Theorem	ancrd 247	Deduction conjoining antecedent to right of consequent in nested implication.
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> (ch /\ ps)))
Theorem	anc2l 248	Conjoin antecedent to left of consequent in nested implication.
|- ((ph -> (ps -> ch)) -> (ph -> (ps -> (ph /\ ch))))
Theorem	anc2r 249	Conjoin antecedent to right of consequent in nested implication.
|- ((ph -> (ps -> ch)) -> (ph -> (ps -> (ch /\ ph))))
Theorem	anc2li 250	Deduction conjoining antecedent to left of consequent in nested implication.
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> (ph /\ ch)))
Theorem	anc2ri 251	Deduction conjoining antecedent to right of consequent in nested implication.
|- (ph -> (ps -> ch))   =>   |- (ph -> (ps -> (ch /\ ph)))
Theorem	anor 252	Conjunction in terms of disjunction (DeMorgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120.
|- ((ph /\ ps) <-> -. (-. ph \/ -. ps))
Theorem	ianor 253	Negated conjunction in terms of disjunction (DeMorgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120.
|- (-. (ph /\ ps) <-> (-. ph \/ -. ps))
Theorem	ioran 254	Negated disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120.
|- (-. (ph \/ ps) <-> (-. ph /\ -. ps))
Theorem	oran 255	Disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.57 of [WhiteheadRussell] p. 120.
|- ((ph \/ ps) <-> -. (-. ph /\ -. ps))
Theorem	pm3.26 256	Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112.
|- ((ph /\ ps) -> ph)
Theorem	pm3.26i 257	Inference eliminating a conjunct.
|- (ph /\ ps)   =>   |- ph
Theorem	pm3.26d 258	Deduction eliminating a conjunct.
|- (ph -> (ps /\ ch))   =>   |- (ph -> ps)
Theorem	pm3.26bd 259	Deduction eliminating a conjunct.
|- (ph <-> (ps /\ ch))   =>   |- (ph -> ps)
Theorem	pm3.27 260	Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112.
|- ((ph /\ ps) -> ps)
Theorem	pm3.27i 261	Inference eliminating a conjunct.
|- (ph /\ ps)   =>   |- ps
Theorem	pm3.27d 262	Deduction eliminating a conjunct.
|- (ph -> (ps /\ ch))   =>   |- (ph -> ch)
Theorem	pm3.27bd 263	Deduction eliminating a conjunct.
|- (ph <-> (ps /\ ch))   =>   |- (ph -> ch)
Theorem	anclb 264	Conjoin antecedent to left of consequent. Theorem *4.7 of [WhiteheadRussell] p. 120.
|- ((ph -> ps) <-> (ph -> (ph /\ ps)))
Theorem	ancrb 265	Conjoin antecedent to right of consequent.
|- ((ph -> ps) <-> (ph -> (ps /\ ph)))
Theorem	pm3.4 266	Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113.
|- ((ph /\ ps) -> (ph -> ps))
Theorem	pm4.45im 267	Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119.
|- (ph <-> (ph /\ (ps -> ph)))
Theorem	anim12i 268	Conjoin antecedents and consequents of two premises.
|- (ph -> ps)   &   |- (ch -> th)   =>   |- ((ph /\ ch) -> (ps /\ th))
Theorem	anim1i 269	Introduce conjunct to both sides of an implication.
|- (ph -> ps)   =>   |- ((ph /\ ch) -> (ps /\ ch))
Theorem	anim2i 270	Introduce conjunct to both sides of an implication.
|- (ph -> ps)   =>   |- ((ch /\ ph) -> (ch /\ ps))
Theorem	orim12i 271	Conjoin antecedents and consequents of two premises.
|- (ph -> ps)   &   |- (ch -> th)   =>   |- ((ph \/ ch) -> (ps \/ th))
Theorem	orim1i 272	Introduce disjunct to both sides of an implication.
|- (ph -> ps)   =>   |- ((ph \/ ch) -> (ps \/ ch))
Theorem	orim2i 273	Introduce disjunct to both sides of an implication.
|- (ph -> ps)   =>   |- ((ch \/ ph) -> (ch \/ ps))
Theorem	jao 274	Disjunction of antecedents. Compare Theorem *3.44 of [WhiteheadRussell] p. 113.
|- ((ph -> ps) -> ((ch -> ps) -> ((ph \/ ch) -> ps)))
Theorem	jaoi 275	Inference disjoining the antecedents of two implications.
|- (ph -> ps)   &   |- (ch -> ps)   =>   |- ((ph \/ ch) -> ps)
Theorem	impexp 276	Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122.
|- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))
Theorem	imp 277	Importation inference.
|- (ph -> (ps -> ch))   =>   |- ((ph /\ ps) -> ch)
Theorem	pm3.35 278	Conjunctive detachment. Theorem *3.35 of [WhiteheadRussell] p. 112.
|- ((ph /\ (ph -> ps)) -> ps)
Theorem	imp3a 279	Importation deduction.
|- (ph -> (ps -> (ch -> th)))   =>   |- (ph -> ((ps /\ ch) -> th))
Theorem	imp31 280	An importation inference.
|- (ph -> (ps -> (ch -> th)))   =>   |- (((ph /\ ps) /\ ch) -> th)