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