Metamath Proof Explorer - mmtheorems7

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 - 601-700 - Page 7 of 58

Type	Label	Description
Statement
Theorem	3mix2 601	Introduction in triple disjunction.
|- (ph -> (ps \/ ph \/ ch))
Theorem	3mix3 602	Introduction in triple disjunction.
|- (ph -> (ps \/ ch \/ ph))
Theorem	3pm3.2i 603	Infer conjunction of premises.
|- ph   &   |- ps   &   |- ch   =>   |- (ph /\ ps /\ ch)
Theorem	3jca 604	Join consequents with conjunction.
|- (ph -> ps)   &   |- (ph -> ch)   &   |- (ph -> th)   =>   |- (ph -> (ps /\ ch /\ th))
Theorem	im3an 605	Join antecedents and consequents with conjunction.
|- (ph -> ps)   &   |- (ch -> th)   &   |- (ta -> et)   =>   |- ((ph /\ ch /\ ta ) -> (ps /\ th /\ et))
Theorem	bi3an 606	Join 3 biconditionals with conjunction.
|- (ph <-> ps)   &   |- (ch <-> th)   &   |- (ta <-> et)   =>   |- ((ph /\ ch /\ ta ) <-> (ps /\ th /\ et))
Theorem	bi3or 607	Join antecedents and consequents with disjunction.
|- (ph <-> ps)   &   |- (ch <-> th)   &   |- (ta <-> et)   =>   |- ((ph \/ ch \/ ta ) <-> (ps \/ th \/ et))
Theorem	3imp 608	Importation inference.
|- (ph -> (ps -> (ch -> th)))   =>   |- ((ph /\ ps /\ ch) -> th)
Theorem	3impa 609	Importation from double to triple conjunction.
|- (((ph /\ ps) /\ ch) -> th)   =>   |- ((ph /\ ps /\ ch) -> th)
Theorem	3impb 610	Importation from double to triple conjunction.
|- ((ph /\ (ps /\ ch)) -> th)   =>   |- ((ph /\ ps /\ ch) -> th)
Theorem	3exp 611	Exportation inference.
|- ((ph /\ ps /\ ch) -> th)   =>   |- (ph -> (ps -> (ch -> th)))
Theorem	3expa 612	Exportation from triple to double conjunction.
|- ((ph /\ ps /\ ch) -> th)   =>   |- (((ph /\ ps) /\ ch) -> th)
Theorem	3expb 613	Exportation from triple to double conjunction.
|- ((ph /\ ps /\ ch) -> th)   =>   |- ((ph /\ (ps /\ ch)) -> th)
Theorem	3com12 614	Commutation in antecedent. Swap 1st and 3rd.
|- ((ph /\ ps /\ ch) -> th)   =>   |- ((ps /\ ph /\ ch) -> th)
Theorem	3com13 615	Commutation in antecedent. Swap 1st and 3rd.
|- ((ph /\ ps /\ ch) -> th)   =>   |- ((ch /\ ps /\ ph) -> th)
Theorem	3com23 616	Commutation in antecedent. Swap 2nd and 3rd.
|- ((ph /\ ps /\ ch) -> th)   =>   |- ((ph /\ ch /\ ps) -> th)
Theorem	3coml 617	Commutation in antecedent. Rotate left.
|- ((ph /\ ps /\ ch) -> th)   =>   |- ((ps /\ ch /\ ph) -> th)
Theorem	3comr 618	Commutation in antecedent. Rotate right.
|- ((ph /\ ps /\ ch) -> th)   =>   |- ((ch /\ ph /\ ps) -> th)
Theorem	syl3an1 619	A syllogism inference.
|- ((ph /\ ps /\ ch) -> th)   &   |- (ta -> ph)   =>   |- ((ta /\ ps /\ ch) -> th)
Theorem	syl3an2 620	A syllogism inference.
|- ((ph /\ ps /\ ch) -> th)   &   |- (ta -> ps)   =>   |- ((ph /\ ta /\ ch) -> th)
Theorem	syl3an3 621	A syllogism inference.
|- ((ph /\ ps /\ ch) -> th)   &   |- (ta -> ch)   =>   |- ((ph /\ ps /\ ta ) -> th)
Theorem	syl3an1b 622	A syllogism inference.
|- ((ph /\ ps /\ ch) -> th)   &   |- (ta <-> ph)   =>   |- ((ta /\ ps /\ ch) -> th)
Theorem	syl3an2b 623	A syllogism inference.
|- ((ph /\ ps /\ ch) -> th)   &   |- (ta <-> ps)   =>   |- ((ph /\ ta /\ ch) -> th)
Theorem	syl3an3b 624	A syllogism inference.
|- ((ph /\ ps /\ ch) -> th)   &   |- (ta <-> ch)   =>   |- ((ph /\ ps /\ ta ) -> th)
Theorem	syl3an1br 625	A syllogism inference.
|- ((ph /\ ps /\ ch) -> th)   &   |- (ph <-> ta )   =>   |- ((ta /\ ps /\ ch) -> th)
Theorem	syl3an2br 626	A syllogism inference.
|- ((ph /\ ps /\ ch) -> th)   &   |- (ps <-> ta )   =>   |- ((ph /\ ta /\ ch) -> th)
Theorem	syl3an3br 627	A syllogism inference.
|- ((ph /\ ps /\ ch) -> th)   &   |- (ch <-> ta )   =>   |- ((ph /\ ps /\ ta ) -> th)
Theorem	syl3an 628	A triple syllogism inference.
|- ((ph /\ ps /\ ch) -> th)   &   |- (ta -> ph)   &   |- (et -> ps)   &   |- (ze -> ch)   =>   |- ((ta /\ et /\ ze) -> th)
Theorem	syl3anc 629	A syllogism inference combined with contraction.
|- ((ph /\ ps /\ ch) -> th)   &   |- (ta -> ph)   &   |- (ta -> ps)   &   |- (ta -> ch)   =>   |- (ta -> th)
Theorem	3impdi 630	Importation inference (undistribute conjunction).
|- (((ph /\ ps) /\ (ph /\ ch)) -> th)   =>   |- ((ph /\ ps /\ ch) -> th)
Theorem	3impdir 631	Importation inference (undistribute conjunction).
|- (((ph /\ ps) /\ (ch /\ ps)) -> th)   =>   |- ((ph /\ ch /\ ps) -> th)
Theorem	3jao 632	Disjunction of 3 antecedents.
|- (((ph -> ps) /\ (ch -> ps) /\ (th -> ps)) -> ((ph \/ ch \/ th) -> ps))
Theorem	3jaoi 633	Disjunction of 3 antecedents (inference).
|- (ph -> ps)   &   |- (ch -> ps)   &   |- (th -> ps)   =>   |- ((ph \/ ch \/ th) -> ps)
Theorem	syl3an9b 634	Nested syllogism inference conjoining 3 dissimilar antecedents.
|- (ph -> (ps <-> ch))   &   |- (th -> (ch <-> ta ))   &   |- (et -> (ta <-> ze))   =>   |- ((ph /\ th /\ et) -> (ps <-> ze))
Theorem	bi3ord 635	Deduction joining 3 equivalences to form equivalence of disjunctions.
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ta ))   &   |- (ph -> (et <-> ze))   =>   |- (ph -> ((ps \/ th \/ et) <-> (ch \/ ta \/ ze)))
Theorem	bi3and 636	Deduction joining 3 equivalences to form equivalence of conjunctions.
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ta ))   &   |- (ph -> (et <-> ze))   =>   |- (ph -> ((ps /\ th /\ et) <-> (ch /\ ta /\ ze)))
Theorem	im3ord 637	Deduction joining 3 implications to form implication of disjunctions.
|- (ph -> (ps -> ch))   &   |- (ph -> (th -> ta ))   &   |- (ph -> (et -> ze))   =>   |- (ph -> ((ps \/ th \/ et) -> (ch \/ ta \/ ze)))
Theorem	an6 638	Rearrangement of 6 conjuncts.
|- (((ph /\ ps /\ ch) /\ (th /\ ta /\ et)) <-> ((ph /\ th) /\ (ps /\ ta ) /\ (ch /\ et)))
Theorem	mp3an1 639	An inference based on modus ponens.
|- ph   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ps /\ ch) -> th)
Theorem	mp3an2 640	An inference based on modus ponens.
|- ps   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ph /\ ch) -> th)
Theorem	mp3an3 641	An inference based on modus ponens.
|- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	mp3an 642	An inference based on modus ponens.
|- ph   &   |- ps   &   |- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- th
Theorem	ecased 643	Deduction for elimination by cases.
|- (ph -> (ps \/ ch \/ th))   &   |- (ph -> -. ch)   &   |- (ph -> -. th)   =>   |- (ph -> ps)
Theorem	meredith 644	Carew Meredith's sole axiom for propositional calculus. This amazing formula is thought to be the shortest possible single axiom for propositional calculus using negation, implication, and inference rule ax-mp 6. Here we prove Meredith's axiom from ax-1 3, ax-2 4, and ax-3 5. Then from it we derive the Lukasiewicz axioms luk-1 658, luk-2 659, and luk-3 660. Using these we finally re-derive our axioms as ax1 669, ax2 670, and ax3 671, thus proving the equivalence of all three systems. C. A. Meredith, "Single Axioms for the Systems (C,N), (C,O) and (A,N) of the Two-Valued Propositional Calculus", The Journal of Computing Systems vol. 3 (1953), pp. 155-164. Meredith claimed to be close to a proof that this axiom is the shortest possible, but the proof was apparently never completed. An obscure Irish lecturer, Meredith (1904-1976) became enamored with logic somewhat late in life after attending talks by Lukasiewicz and produced many remarkable results such as this axiom. From his obituary: "He did logic whenever time and opportunity presented themselves, and he did it on whatever materials came to hand: in a pub, his favored pint of porter within reach, he would use the inside of cigarette packs to write proofs for logical colleagues."
|- (((((ph -> ps) -> (-. ch -> -. th)) -> ch) -> ta ) -> ((ta -> ph) -> (th -> ph)))
Theorem	merlem1 645	Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (The step numbers refer to Meredith's original paper.)
|- (((ch -> (-. ph -> ps)) -> ta ) -> (ph -> ta ))
Theorem	merlem2 646	Step 4 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((ph -> ph) -> ch) -> (th -> ch))
Theorem	merlem3 647	Step 7 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((ps -> ch) -> ph) -> (ch -> ph))
Theorem	merlem4 648	Step 8 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (ta -> ((ta -> ph) -> (th -> ph)))
Theorem	merlem5 649	Step 11 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- ((ph -> ps) -> (-. -. ph -> ps))
Theorem	merlem6 650	Step 12 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (ch -> (((ps -> ch) -> ph) -> (th -> ph)))
Theorem	merlem7 651	Between steps 14 and 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (ph -> (((ps -> ch) -> th) -> (((ch -> ta ) -> (-. th -> -. ps)) -> th)))
Theorem	merlem8 652	Step 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((ps -> ch) -> th) -> (((ch -> ta ) -> (-. th -> -. ps)) -> th))
Theorem	merlem9 653	Step 18 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- (((ph -> ps) -> (ch -> (th -> (ps -> ta )))) -> (et -> (ch -> (th -> (ps -> ta )))))
Theorem	merlem10 654	Step 19 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
|- ((ph -> (ph ->