mmtheorems6 - 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-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

Statement List for Metamath Proof Explorer - 501-600 - Page 6 of 175

Type	Label	Description
Statement
Theorem	sylan2b 501	A syllogism inference.
|- ((ph /\ ps) -> ch)   &   |- (th <-> ps)   =>   |- ((ph /\ th) -> ch)
Theorem	sylan2br 502	A syllogism inference.
|- ((ph /\ ps) -> ch)   &   |- (ps <-> th)   =>   |- ((ph /\ th) -> ch)
Theorem	syl2an 503	A double syllogism inference.
|- ((ph /\ ps) -> ch)   &   |- (th -> ph)   &   |- (ta -> ps)   =>   |- ((th /\ ta) -> ch)
Theorem	syl2anb 504	A double syllogism inference.
|- ((ph /\ ps) -> ch)   &   |- (th <-> ph)   &   |- (ta <-> ps)   =>   |- ((th /\ ta) -> ch)
Theorem	syl2anbr 505	A double syllogism inference.
|- ((ph /\ ps) -> ch)   &   |- (ph <-> th)   &   |- (ps <-> ta)   =>   |- ((th /\ ta) -> ch)
Theorem	syland 506	A syllogism deduction.
|- (ph -> ((ps /\ ch) -> th))   &   |- (ph -> (ta -> ps))   =>   |- (ph -> ((ta /\ ch) -> th))
Theorem	sylan2d 507	A syllogism deduction.
|- (ph -> ((ps /\ ch) -> th))   &   |- (ph -> (ta -> ch))   =>   |- (ph -> ((ps /\ ta) -> th))
Theorem	syl2and 508	A syllogism deduction.
|- (ph -> ((ps /\ ch) -> th))   &   |- (ph -> (ta -> ps))   &   |- (ph -> (et -> ch))   =>   |- (ph -> ((ta /\ et) -> th))
Theorem	sylanl1 509	A syllogism inference.
|- (((ph /\ ps) /\ ch) -> th)   &   |- (ta -> ph)   =>   |- (((ta /\ ps) /\ ch) -> th)
Theorem	sylanl2 510	A syllogism inference.
|- (((ph /\ ps) /\ ch) -> th)   &   |- (ta -> ps)   =>   |- (((ph /\ ta) /\ ch) -> th)
Theorem	sylanr1 511	A syllogism inference.
|- ((ph /\ (ps /\ ch)) -> th)   &   |- (ta -> ps)   =>   |- ((ph /\ (ta /\ ch)) -> th)
Theorem	sylanr2 512	A syllogism inference.
|- ((ph /\ (ps /\ ch)) -> th)   &   |- (ta -> ch)   =>   |- ((ph /\ (ps /\ ta)) -> th)
Theorem	sylani 513	A syllogism inference.
|- (ph -> ((ps /\ ch) -> th))   &   |- (ta -> ps)   =>   |- (ph -> ((ta /\ ch) -> th))
Theorem	sylan2i 514	A syllogism inference.
|- (ph -> ((ps /\ ch) -> th))   &   |- (ta -> ch)   =>   |- (ph -> ((ps /\ ta) -> th))
Theorem	syl2ani 515	A syllogism inference.
|- (ph -> ((ps /\ ch) -> th))   &   |- (ta -> ps)   &   |- (et -> ch)   =>   |- (ph -> ((ta /\ et) -> th))
Theorem	syldan 516	A syllogism deduction with conjoined antecents.
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ ch) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	sylan9 517	Nested syllogism inference conjoining dissimilar antecedents. (The proof was shortened by Andrew Salmon, 7-May-2011.)
|- (ph -> (ps -> ch))   &   |- (th -> (ch -> ta))   =>   |- ((ph /\ th) -> (ps -> ta))
Theorem	sylan9OLD 518	Nested syllogism inference conjoining dissimilar antecedents.
|- (ph -> (ps -> ch))   &   |- (th -> (ch -> ta))   =>   |- ((ph /\ th) -> (ps -> ta))
Theorem	sylan9r 519	Nested syllogism inference conjoining dissimilar antecedents.
|- (ph -> (ps -> ch))   &   |- (th -> (ch -> ta))   =>   |- ((th /\ ph) -> (ps -> ta))
Theorem	mtand 520	A modus tollens deduction. (Contributed by Jeff Hankins, 19-Aug-2009.)
|- (ph -> -. ch)   &   |- ((ph /\ ps) -> ch)   =>   |- (ph -> -. ps)
Theorem	mpan9 521	Modus ponens conjoining dissimilar antecedents. (The proof was shortened by Andrew Salmon, 7-May-2011.)
|- (ph -> ps)   &   |- (ch -> (ps -> th))   =>   |- ((ph /\ ch) -> th)
Theorem	mpan9OLD 522	Modus ponens conjoining dissimilar antecedents.
|- (ph -> ps)   &   |- (ch -> (ps -> th))   =>   |- ((ph /\ ch) -> th)
Theorem	sylancOLD 523	A syllogism inference combined with contraction. (OBSOLETE - replaced by syl11anc 524 21-Mar-2012. --NM)
|- ((ph /\ ps) -> ch)   &   |- (th -> ph)   &   |- (th -> ps)   =>   |- (th -> ch)
Theorem	syl11anc 524	Syllogism inference combined with contraction.
|- (ph -> ps)   &   |- (ph -> ch)   &   |- ((ps /\ ch) -> th)   =>   |- (ph -> th)
Theorem	sylancl 525	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ((ph /\ ps) -> ch)   &   |- (th -> ph)   &   |- ps   =>   |- (th -> ch)
Theorem	sylancr 526	Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ((ph /\ ps) -> ch)   &   |- ph   &   |- (th -> ps)   =>   |- (th -> ch)
Theorem	sylanbrc 527	Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)
|- (ph <-> (ps /\ ch))   &   |- (th -> ps)   &   |- (th -> ch)   =>   |- (th -> ph)
Theorem	syl2ancOLD 528	A syllogism inference combined with contraction. (OBSOLETE - replaced by syl22anc 1101 21-Mar-2012. --NM)
|- (((ph /\ ps) /\ (ch /\ th)) -> ta)   &   |- (et -> ph)   &   |- (et -> ps)   &   |- (et -> ch)   &   |- (et -> th)   =>   |- (et -> ta)
Theorem	sylancb 529	A syllogism inference combined with contraction.
|- ((ph /\ ps) -> ch)   &   |- (th <-> ph)   &   |- (th <-> ps)   =>   |- (th -> ch)
Theorem	sylancbr 530	A syllogism inference combined with contraction.
|- ((ph /\ ps) -> ch)   &   |- (ph <-> th)   &   |- (ps <-> th)   =>   |- (th -> ch)
Theorem	sylancom 531	Syllogism inference with commutation of antecents.
|- ((ph /\ ps) -> ch)   &   |- ((ch /\ ps) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	sylan31cOLD 532	A syllogism inference combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.) (OBSOLETE - replaced by syl21anc 1099 21-Mar-2012. --NM)
|- (ta -> ph)   &   |- (ta -> ps)   &   |- (ta -> ch)   &   |- (((ph /\ ps) /\ ch) -> th)   =>   |- (ta -> th)
Theorem	sylan32cOLD 533	A syllogism inference combined with contraction. (Contributed by Jeff Hankins, 1-Aug-2009.) (OBSOLETE - replaced by syl12anc 1098 21-Mar-2012. --NM)
|- (ta -> ph)   &   |- (ta -> ps)   &   |- (ta -> ch)   &   |- ((ph /\ (ps /\ ch)) -> th)   =>   |- (ta -> th)
Theorem	pm2.61ian 534	Elimination of an antecedent.
|- ((ph /\ ps) -> ch)   &   |- ((-. ph /\ ps) -> ch)   =>   |- (ps -> ch)
Theorem	pm2.61dan 535	Elimination of an antecedent.
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ -. ps) -> ch)   =>   |- (ph -> ch)
Theorem	condan 536	Proof by contradiction.
|- ((ph /\ -. ps) -> ch)   &   |- ((ph /\ -. ps) -> -. ch)   =>   |- (ph -> ps)
Theorem	abai 537	Introduce one conjunct as an antecedent to the another.
|- ((ph /\ ps) <-> (ph /\ (ph -> ps)))
Theorem	anbi2i 538	Introduce a left conjunct to both sides of a logical equivalence.
|- (ph <-> ps)   =>   |- ((ch /\ ph) <-> (ch /\ ps))
Theorem	anbi1i 539	Introduce a right conjunct to both sides of a logical equivalence.
|- (ph <-> ps)   =>   |- ((ph /\ ch) <-> (ps /\ ch))
Theorem	anbi12i 540	Conjoin both sides of two equivalences.
|- (ph <-> ps)   &   |- (ch <-> th)   =>   |- ((ph /\ ch) <-> (ps /\ th))
Theorem	pm5.53 541	Theorem *5.53 of [WhiteheadRussell] p. 125.
|- ((((ph \/ ps) \/ ch) -> th) <-> (((ph -> th) /\ (ps -> th)) /\ (ch -> th)))
Theorem	an12 542	A rearrangement of conjuncts.
|- ((ph /\ (ps /\ ch)) <-> (ps /\ (ph /\ ch)))
Theorem	an23 543	A rearrangement of conjuncts.
|- (((ph /\ ps) /\ ch) <-> ((ph /\ ch) /\ ps))
Theorem	an1s 544	Deduction rearranging conjuncts.
|- ((ph /\ (ps /\ ch)) -> th)   =>   |- ((ps /\ (ph /\ ch)) -> th)
Theorem	ancom2s 545	Inference commuting a nested conjunction in antecedent.
|- ((ph /\ (ps /\ ch)) -> th)   =>   |- ((ph /\ (ch /\ ps)) -> th)
Theorem	ancom13s 546	Deduction rearranging conjuncts.
|- ((ph /\ (ps /\ ch)) -> th)   =>   |- ((ch /\ (ps /\ ph)) -> th)
Theorem	an1rs 547	Deduction rearranging conjuncts.
|- (((ph /\ ps) /\ ch) -> th)   =>   |- (((ph /\ ch) /\ ps) -> th)
Theorem	ancom1s 548	Inference commuting a nested conjunction in antecedent.
|- (((ph /\ ps) /\ ch) -> th)   =>   |- (((ps /\ ph) /\ ch) -> th)
Theorem	ancom31s 549	Deduction rearranging conjuncts.
|- (((ph /\ ps) /\ ch) -> th)   =>   |- (((ch /\ ps) /\ ph) -> th)
Theorem	anabs1 550	Absorption into embedded conjunct.
|- (((ph /\ ps) /\ ph) <-> (ph /\ ps))
Theorem	anabs5 551	Absorption into embedded conjunct.
|- ((ph /\ (ph /\ ps)) <-> (ph /\ ps))
Theorem	anabs7 552	Absorption into embedded conjunct.
|- ((ps /\ (ph /\ ps)) <-> (ph /\ ps))
Theorem	anabsi5 553	Absorption of antecedent into conjunction.
|- (ph -> ((ph /\ ps) -> ch))   =>   |- ((ph /\ ps) -> ch)
Theorem	anabsi6 554	Absorption of antecedent into conjunction.
|- (ph -> ((ps /\ ph) -> ch))   =>   |- ((ph /\ ps) -> ch)
Theorem	anabsi7 555	Absorption of antecedent into conjunction.
|- (ps -> ((ph /\ ps) -> ch))   =>   |- ((ph /\ ps) -> ch)
Theorem	anabsi8 556	Absorption of antecedent into conjunction.
|- (ps -> ((ps /\ ph) -> ch))   =>   |- ((ph /\ ps) -> ch)
Theorem	anabss1 557	Absorption of antecedent into conjunction.
|- (((ph /\ ps) /\ ph) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	anabss3 558	Absorption of antecedent into conjunction.
|- (((ph /\ ps) /\ ps) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	anabss4 559	Absorption of antecedent into conjunction.
|- (((ps /\ ph) /\ ps) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	anabss5 560	Absorption of antecedent into conjunction.
|- ((ph /\ (ph /\ ps)) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	anabss7 561	Absorption of antecedent into conjunction.
|- ((ps /\ (ph /\ ps)) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	anabsan 562	Absorption of antecedent with conjunction.
|- (((ph /\ ph) /\ ps) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	anabsan2 563	Absorption of antecedent with conjunction.
|- ((ph /\ (ps /\ ps)) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	an4 564	Rearrangement of 4 conjuncts.
|- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (ps /\ th)))
Theorem	an42 565	Rearrangement of 4 conjuncts.
|- (((ph /\ ps) /\ (ch /\ th)) <-> ((ph /\ ch) /\ (th /\ ps)))
Theorem	an4s 566	Inference rearranging 4 conjuncts in antecedent.
|- (((ph /\ ps) /\ (ch /\ th)) -> ta)   =>   |- (((ph /\ ch) /\ (ps /\ th)) -> ta)
Theorem	an42s 567	Inference rearranging 4 conjuncts in antecedent.
|- (((ph /\ ps) /\ (ch /\ th)) -> ta)   =>   |- (((ph /\ ch) /\ (th /\ ps)) -> ta)
Theorem	anandi 568	Distribution of conjunction over conjunction.
|- ((ph /\ (ps /\ ch)) <-> ((ph /\ ps) /\ (ph /\ ch)))
Theorem	anandir 569	Distribution of conjunction over conjunction.
|- (((ph /\ ps) /\ ch) <-> ((ph /\ ch) /\ (ps /\ ch)))
Theorem	anandis 570	Inference that undistributes conjunction in the antecedent.
|- (((ph /\ ps) /\ (ph /\ ch)) -> ta)   =>   |- ((ph /\ (ps /\ ch)) -> ta)
Theorem	anandirs 571	Inference that undistributes conjunction in the antecedent.
|- (((ph /\ ch) /\ (ps /\ ch)) -> ta)   =>   |- (((ph /\ ps) /\ ch) -> ta)
Theorem	dfbi2 572	A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49.
|- ((ph <-> ps) <-> ((ph -> ps) /\ (ps -> ph)))
Theorem	dfbi 573	Definition df-bi 164 rewritten in an abbreviated form to help intuitive understanding of that definition. Note that it is a conjunction of two implications; one which asserts properties that follow from the biconditional and one which asserts properties that imply the biconditional.
|- (((ph <-> ps) -> ((ph -> ps) /\ (ps -> ph))) /\ (((ph -> ps) /\ (ps -> ph)) -> (ph <-> ps)))
Theorem	impbid 574	Deduce an equivalence from two implications.
|- (ph -> (ps -> ch))   &   |- (ph -> (ch -> ps))   =>   |- (ph -> (ps <-> ch))
Theorem	impbid1 575	Infer an equivalence from two implications.
|- (ph -> (ps -> ch))   &   |- (ch -> ps)   =>   |- (ph -> (ps <-> ch))
Theorem	impbid2 576	Infer an equivalence from two implications.
|- (ps -> ch)   &   |- (ph -> (ch -> ps))   =>   |- (ph -> (ps <-> ch))
Theorem	impbida 577	Deduce an equivalence from two implications.
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ ch) -> ps)   =>   |- (ph -> (ps <-> ch))
Theorem	impcon4bid 578	A variation on impbid 574 with contraposition. (Contributed by Jeff Hankins, 3-Jul-2009.)
|- (ph -> (ps -> ch))   &   |- (ph -> (-. ps -> -. ch))   =>   |- (ph -> (ps <-> ch))
Theorem	bicom 579	Commutative law for equivalence. Theorem *4.21 of [WhiteheadRussell] p. 117.
|- ((ph <-> ps) <-> (ps <-> ph))
Theorem	bicomd 580	Commute two sides of a biconditional in a deduction.
|- (ph -> (ps <-> ch))   =>   |- (ph -> (ch <-> ps))
Theorem	notbi 581	Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117.
|- ((ph <-> ps) <-> (-. ph <-> -. ps))
Theorem	con4bii 582	A contraposition inference.
|- (-. ph <-> -. ps)   =>   |- (ph <-> ps)
Theorem	con4bid 583	A contraposition deduction.
|- (ph -> (-. ps <-> -. ch))   =>   |- (ph -> (ps <-> ch))
Theorem	con2bi 584	Contraposition. Theorem *4.12 of [WhiteheadRussell] p. 117.
|- ((ph <-> -. ps) <-> (ps <-> -. ph))
Theorem	con2bid 585	A contraposition deduction.
|- (ph -> (ps <-> -. ch))   =>   |- (ph -> (ch <-> -. ps))
Theorem	con1bid 586	A contraposition deduction.
|- (ph -> (-. ps <-> ch))   =>   |- (ph -> (-. ch <-> ps))
Theorem	bitrd 587	Deduction form of bitri 190.
|- (ph -> (ps <-> ch))   &   |- (ph -> (ch <-> th))   =>   |- (ph -> (ps <-> th))
Theorem	bitr2d 588	Deduction form of bitr2i 191.
|- (ph -> (ps <-> ch))   &   |- (ph -> (ch <-> th))   =>   |- (ph -> (th <-> ps))
Theorem	bitr3d 589	Deduction form of bitr3i 192.
|- (ph -> (ps <-> ch))   &   |- (ph -> (ps <-> th))   =>   |- (ph -> (ch <-> th))
Theorem	bitr4d 590	Deduction form of bitr4i 193.
|- (ph -> (ps <-> ch))   &   |- (ph -> (th <-> ch))   =>   |- (ph -> (ps <-> th))
Theorem	syl5bb 591	A syllogism inference from two biconditionals.
|- (ph -> (ps <-> ch))   &   |- (th <-> ps)   =>   |- (ph -> (th <-> ch))
Theorem	syl5rbb 592	A syllogism inference from two biconditionals.
|- (ph -> (ps <-> ch))   &   |- (th <-> ps)   =>   |- (ph -> (ch <-> th))
Theorem	syl5bbr 593	A syllogism inference from two biconditionals.
|- (ph -> (ps <-> ch))   &   |- (ps <-> th)   =>   |- (ph -> (th <-> ch))
Theorem	syl5rbbr 594	A syllogism inference from two biconditionals.
|- (ph -> (ps <-> ch))   &   |- (ps <-> th)   =>   |- (ph -> (ch <-> th))
Theorem	syl6bb 595	A syllogism inference from two biconditionals.
|- (ph -> (ps <-> ch))   &   |- (ch <-> th)   =>   |- (ph -> (ps <-> th))
Theorem	syl6rbb 596	A syllogism inference from two biconditionals.
|- (ph -> (ps <-> ch))   &   |- (ch <-> th)   =>   |- (ph -> (th <-> ps))
Theorem	syl6bbr 597	A syllogism inference from two biconditionals.
|- (ph -> (ps <-> ch))   &   |- (th <-> ch)   =>   |- (ph -> (ps <-> th))
Theorem	syl6rbbr 598	A syllogism inference from two biconditionals.
|- (ph -> (ps <-> ch))   &   |- (th <-> ch)   =>   |- (ph -> (th <-> ps))
Theorem	sylan9bb 599	Nested syllogism inference conjoining dissimilar antecedents.
|- (ph -> (ps <-> ch))   &   |- (th -> (ch <-> ta))   =>   |- ((ph /\ th) -> (ps <-> ta))
Theorem	sylan9bbr 600	Nested syllogism inference conjoining dissimilar antecedents.
|- (ph -> (ps <-> ch))   &   |- (th -> (ch <-> ta))   =>   |- ((th /\ ph) -> (ps <-> ta))