 Home New Foundations ExplorerTheorem List (p. 9 of 64) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 801-900   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremanandi 801 Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
((φ (ψ χ)) ↔ ((φ ψ) (φ χ)))

Theoremanandir 802 Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)
(((φ ψ) χ) ↔ ((φ χ) (ψ χ)))

Theoremanandis 803 Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
(((φ ψ) (φ χ)) → τ)       ((φ (ψ χ)) → τ)

Theoremanandirs 804 Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
(((φ χ) (ψ χ)) → τ)       (((φ ψ) χ) → τ)

Theoremimpbida 805 Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
((φ ψ) → χ)    &   ((φ χ) → ψ)       (φ → (ψχ))

Theorempm3.48 806 Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.)
(((φψ) (χθ)) → ((φ χ) → (ψ θ)))

Theorempm3.45 807 Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
((φψ) → ((φ χ) → (ψ χ)))

Theoremim2anan9 808 Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
(φ → (ψχ))    &   (θ → (τη))       ((φ θ) → ((ψ τ) → (χ η)))

Theoremim2anan9r 809 Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
(φ → (ψχ))    &   (θ → (τη))       ((θ φ) → ((ψ τ) → (χ η)))

Theoremanim12dan 810 Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)
((φ ψ) → χ)    &   ((φ θ) → τ)       ((φ (ψ θ)) → (χ τ))

Theoremorim12d 811 Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)
(φ → (ψχ))    &   (φ → (θτ))       (φ → ((ψ θ) → (χ τ)))

Theoremorim1d 812 Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
(φ → (ψχ))       (φ → ((ψ θ) → (χ θ)))

Theoremorim2d 813 Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
(φ → (ψχ))       (φ → ((θ ψ) → (θ χ)))

Theoremorim2 814 Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.)
((ψχ) → ((φ ψ) → (φ χ)))

Theorempm2.38 815 Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
((ψχ) → ((ψ φ) → (χ φ)))

Theorempm2.36 816 Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
((ψχ) → ((φ ψ) → (χ φ)))

Theorempm2.37 817 Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
((ψχ) → ((ψ φ) → (φ χ)))

Theorempm2.73 818 Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
((φψ) → (((φ ψ) χ) → (ψ χ)))

Theorempm2.74 819 Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.)
((ψφ) → (((φ ψ) χ) → (φ χ)))

Theoremorimdi 820 Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013.)
((φ (ψχ)) ↔ ((φ ψ) → (φ χ)))

Theorempm2.76 821 Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
((φ (ψχ)) → ((φ ψ) → (φ χ)))

Theorempm2.75 822 Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.)
((φ ψ) → ((φ (ψχ)) → (φ χ)))

Theorempm2.8 823 Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
((φ ψ) → ((¬ ψ χ) → (φ χ)))

Theorempm2.81 824 Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
((ψ → (χθ)) → ((φ ψ) → ((φ χ) → (φ θ))))

Theorempm2.82 825 Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
(((φ ψ) χ) → (((φ ¬ χ) θ) → ((φ ψ) θ)))

Theorempm2.85 826 Theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
(((φ ψ) → (φ χ)) → (φ (ψχ)))

Theorempm3.2ni 827 Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.)
¬ φ    &    ¬ ψ        ¬ (φ ψ)

Theoremorabs 828 Absorption of redundant internal disjunct. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 28-Feb-2014.)
(φ ↔ ((φ ψ) φ))

Theoremoranabs 829 Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.)
(((φ ¬ ψ) ψ) ↔ (φ ψ))

Theorempm5.1 830 Two propositions are equivalent if they are both true. Theorem *5.1 of [WhiteheadRussell] p. 123. (Contributed by NM, 21-May-1994.)
((φ ψ) → (φψ))

Theorempm5.21 831 Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124. (Contributed by NM, 21-May-1994.)
((¬ φ ¬ ψ) → (φψ))

Theorempm3.43 832 Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
(((φψ) (φχ)) → (φ → (ψ χ)))

Theoremjcab 833 Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 27-Nov-2013.)
((φ → (ψ χ)) ↔ ((φψ) (φχ)))

Theoremordi 834 Distributive law for disjunction. Theorem *4.41 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 28-Nov-2013.)
((φ (ψ χ)) ↔ ((φ ψ) (φ χ)))

Theoremordir 835 Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
(((φ ψ) χ) ↔ ((φ χ) (ψ χ)))

Theorempm4.76 836 Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
(((φψ) (φχ)) ↔ (φ → (ψ χ)))

Theoremandi 837 Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
((φ (ψ χ)) ↔ ((φ ψ) (φ χ)))

Theoremandir 838 Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
(((φ ψ) χ) ↔ ((φ χ) (ψ χ)))

Theoremorddi 839 Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
(((φ ψ) (χ θ)) ↔ (((φ χ) (φ θ)) ((ψ χ) (ψ θ))))

Theoremanddi 840 Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
(((φ ψ) (χ θ)) ↔ (((φ χ) (φ θ)) ((ψ χ) (ψ θ))))

Theorempm4.39 841 Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
(((φχ) (ψθ)) → ((φ ψ) ↔ (χ θ)))

Theorempm4.38 842 Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
(((φχ) (ψθ)) → ((φ ψ) ↔ (χ θ)))

Theorembi2anan9 843 Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)
(φ → (ψχ))    &   (θ → (τη))       ((φ θ) → ((ψ τ) ↔ (χ η)))

Theorembi2anan9r 844 Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.)
(φ → (ψχ))    &   (θ → (τη))       ((θ φ) → ((ψ τ) ↔ (χ η)))

Theorembi2bian9 845 Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004.)
(φ → (ψχ))    &   (θ → (τη))       ((φ θ) → ((ψτ) ↔ (χη)))

Theorempm4.72 846 Implication in terms of biconditional and disjunction. Theorem *4.72 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jan-2013.)
((φψ) ↔ (ψ ↔ (φ ψ)))

Theoremimimorb 847 Simplify an implication between implications. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)
(((ψχ) → (φχ)) ↔ (φ → (ψ χ)))

Theorempm5.33 848 Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
((φ (ψχ)) ↔ (φ ((φ ψ) → χ)))

Theorempm5.36 849 Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
((φ (φψ)) ↔ (ψ (φψ)))

Theorembianabs 850 Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.)
(φ → (ψ ↔ (φ χ)))       (φ → (ψχ))

Theoremoibabs 851 Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)
(((φ ψ) → (φψ)) ↔ (φψ))

Theorempm3.24 852 Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who call it the "law of contradiction"). (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
¬ (φ ¬ φ)

Theorempm2.26 853 Theorem *2.26 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
φ ((φψ) → ψ))

Theorempm5.11 854 Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
((φψ) φψ))

Theorempm5.12 855 Theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
((φψ) (φ → ¬ ψ))

Theorempm5.14 856 Theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
((φψ) (ψχ))

Theorempm5.13 857 Theorem *5.13 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
((φψ) (ψφ))

Theorempm5.17 858 Theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Jan-2013.)
(((φ ψ) ¬ (φ ψ)) ↔ (φ ↔ ¬ ψ))

Theorempm5.15 859 Theorem *5.15 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 15-Oct-2013.)
((φψ) (φ ↔ ¬ ψ))

Theorempm5.16 860 Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 17-Oct-2013.)
¬ ((φψ) (φ ↔ ¬ ψ))

Theoremxor 861 Two ways to express "exclusive or." Theorem *5.22 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 22-Jan-2013.)
(¬ (φψ) ↔ ((φ ¬ ψ) (ψ ¬ φ)))

Theoremnbi2 862 Two ways to express "exclusive or." (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)
(¬ (φψ) ↔ ((φ ψ) ¬ (φ ψ)))

Theoremdfbi3 863 An alternate definition of the biconditional. Theorem *5.23 of [WhiteheadRussell] p. 124. (Contributed by NM, 27-Jun-2002.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)
((φψ) ↔ ((φ ψ) φ ¬ ψ)))

Theorempm5.24 864 Theorem *5.24 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.)
(¬ ((φ ψ) φ ¬ ψ)) ↔ ((φ ¬ ψ) (ψ ¬ φ)))

Theoremxordi 865 Conjunction distributes over exclusive-or, using ¬ (φψ) to express exclusive-or. This is one way to interpret the distributive law of multiplication over addition in modulo 2 arithmetic. (Contributed by NM, 3-Oct-2008.)
((φ ¬ (ψχ)) ↔ ¬ ((φ ψ) ↔ (φ χ)))

Theorembiort 866 A wff disjoined with truth is true. (Contributed by NM, 23-May-1999.)
(φ → (φ ↔ (φ ψ)))

Theorempm5.55 867 Theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 20-Jan-2013.)
(((φ ψ) ↔ φ) ((φ ψ) ↔ ψ))

1.2.7  Miscellaneous theorems of propositional calculus

Theorempm5.21nd 868 Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.)
((φ ψ) → θ)    &   ((φ χ) → θ)    &   (θ → (ψχ))       (φ → (ψχ))

Theorempm5.35 869 Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
(((φψ) (φχ)) → (φ → (ψχ)))

Theorempm5.54 870 Theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 7-Nov-2013.)
(((φ ψ) ↔ φ) ((φ ψ) ↔ ψ))

Theorembaib 871 Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
(φ ↔ (ψ χ))       (ψ → (φχ))

Theorembaibr 872 Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
(φ ↔ (ψ χ))       (ψ → (χφ))

Theoremrbaib 873 Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
(φ ↔ (ψ χ))       (χ → (φψ))

Theoremrbaibr 874 Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
(φ ↔ (ψ χ))       (χ → (ψφ))

Theorembaibd 875 Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
(φ → (ψ ↔ (χ θ)))       ((φ χ) → (ψθ))

Theoremrbaibd 876 Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
(φ → (ψ ↔ (χ θ)))       ((φ θ) → (ψχ))

Theorempm5.44 877 Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
((φψ) → ((φχ) ↔ (φ → (ψ χ))))

Theorempm5.6 878 Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [WhiteheadRussell] p. 125. (Contributed by NM, 8-Jun-1994.)
(((φ ¬ ψ) → χ) ↔ (φ → (ψ χ)))

Theoremorcanai 879 Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
(φ → (ψ χ))       ((φ ¬ ψ) → χ)

Theoremintnan 880 Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
¬ φ        ¬ (ψ φ)

Theoremintnanr 881 Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
¬ φ        ¬ (φ ψ)

Theoremintnand 882 Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
(φ → ¬ ψ)       (φ → ¬ (χ ψ))

Theoremintnanrd 883 Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
(φ → ¬ ψ)       (φ → ¬ (ψ χ))

Theoremmpbiran 884 Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.)
ψ    &   (φ ↔ (ψ χ))       (φχ)

Theoremmpbiran2 885 Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)
χ    &   (φ ↔ (ψ χ))       (φψ)

Theoremmpbir2an 886 Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.)
ψ    &   χ    &   (φ ↔ (ψ χ))       φ

Theoremmpbi2and 887 Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
(φψ)    &   (φχ)    &   (φ → ((ψ χ) ↔ θ))       (φθ)

Theoremmpbir2and 888 Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
(φχ)    &   (φθ)    &   (φ → (ψ ↔ (χ θ)))       (φψ)

Theorempm5.62 889 Theorem *5.62 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.)
(((φ ψ) ¬ ψ) ↔ (φ ¬ ψ))

Theorempm5.63 890 Theorem *5.63 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
((φ ψ) ↔ (φ φ ψ)))

Theorembianfi 891 A wff conjoined with falsehood is false. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
¬ φ       (φ ↔ (ψ φ))

Theorembianfd 892 A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.)
(φ → ¬ ψ)       (φ → (ψ ↔ (ψ χ)))

Theorempm4.43 893 Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
(φ ↔ ((φ ψ) (φ ¬ ψ)))

Theorempm4.82 894 Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
(((φψ) (φ → ¬ ψ)) ↔ ¬ φ)

Theorempm4.83 895 Theorem *4.83 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
(((φψ) φψ)) ↔ ψ)

Theorempclem6 896 Negation inferred from embedded conjunct. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Nov-2012.)
((φ ↔ (ψ ¬ φ)) → ¬ ψ)

Theorembiantr 897 A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.)
(((φψ) (χψ)) → (φχ))

Theoremorbidi 898 Disjunction distributes over the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.3384. (Contributed by NM, 8-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Feb-2013.)
((φ (ψχ)) ↔ ((φ ψ) ↔ (φ χ)))

Theorembiluk 899 Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed., Polish Logic 1920-1939 (Oxford, 1967), p. 96. (Contributed by NM, 10-Jan-2005.)
((φψ) ↔ ((χψ) ↔ (φχ)))

Theorempm5.7 900 Disjunction distributes over the biconditional. Theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbidi 898. (Contributed by Roy F. Longton, 21-Jun-2005.)
(((φ χ) ↔ (ψ χ)) ↔ (χ (φψ)))

Page List
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-800801-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-6336
 Copyright terms: Public domain < Previous  Next >