Statement List for Metamath Proof Explorer - 101-200 - Page 2 of 58
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | mt3d 101 |
Modus tollens deduction.
|
| ⊢
(φ → ¬ χ)
& ⊢ (φ → (¬ ψ → χ))
⇒ ⊢ (φ → ψ) |
| |
| Theorem | nsyl 102 |
A negated syllogism inference.
|
| ⊢
(φ → ¬ ψ)
& ⊢ (χ → ψ)
⇒ ⊢ (φ → ¬ χ) |
| |
| Theorem | nsyl2 103 |
A negated syllogism inference.
|
| ⊢
(φ → ¬ ψ)
& ⊢ (¬ χ → ψ)
⇒ ⊢ (φ → χ) |
| |
| Theorem | nsyl3 104 |
A negated syllogism inference.
|
| ⊢
(φ → ¬ ψ)
& ⊢ (χ → ψ)
⇒ ⊢ (χ → ¬ φ) |
| |
| Theorem | nsyl4 105 |
A negated syllogism inference.
|
| ⊢
(φ → ψ)
& ⊢ (¬ φ → χ)
⇒ ⊢ (¬ χ → ψ) |
| |
| Theorem | nsyli 106 |
A negated syllogism inference.
|
| ⊢
(φ → (ψ → χ))
& ⊢ (θ → ¬ χ)
⇒ ⊢ (φ → (θ → ¬ ψ)) |
| |
| Theorem | pm3.2im 107 |
Theorem *3.2 of [WhiteheadRussell] p.
111, expressed with primitive
connectives. (The proof was shortened by Josh Purinton, 29-Dec-00.)
|
| ⊢
(φ → (ψ → ¬ (φ → ¬ ψ))) |
| |
| Theorem | mth8 108 |
Theorem 8 of [Margaris] p. 60. (The proof
was shortened by Josh Purinton,
29-Dec-00.)
|
| ⊢
(φ → (¬ ψ → ¬ (φ → ψ))) |
| |
| Theorem | pm2.61 109 |
Theorem *2.61 of [WhiteheadRussell]
p. 107. Useful for eliminating an
antecedent.
|
| ⊢
((φ → ψ) → ((¬ φ → ψ) → ψ)) |
| |
| Theorem | pm2.61i 110 |
Inference eliminating an antecedent.
|
| ⊢
(φ → ψ)
& ⊢ (¬ φ → ψ)
⇒ ⊢ ψ |
| |
| Theorem | pm2.61d2 111 |
Inference eliminating an antecedent.
|
| ⊢
(φ → (¬ ψ → χ))
& ⊢ (ψ → χ)
⇒ ⊢ (φ → χ) |
| |
| Theorem | pm2.61d 112 |
Deduction eliminating an antecedent.
|
| ⊢
(φ → (ψ → χ))
& ⊢ (φ → (¬ ψ → χ))
⇒ ⊢ (φ → χ) |
| |
| Theorem | pm2.61ii 113 |
Inference eliminating two antecedents. (The proof was shortened by Josh
Purinton, 29-Dec-00.)
|
| ⊢
(¬ φ → (¬ ψ → χ))
& ⊢ (φ → χ)
& ⊢ (ψ → χ)
⇒ ⊢ χ |
| |
| Theorem | pm2.61iii 114 |
Inference eliminating three antecedents.
|
| ⊢
(¬ φ → (¬ ψ → (¬ χ → θ)))
& ⊢ (φ → θ)
& ⊢ (ψ → θ)
& ⊢ (χ → θ)
⇒ ⊢ θ |
| |
| Theorem | pm2.65 115 |
Theorem *2.65 of [WhiteheadRussell]
p. 107. Useful for eliminating a
consequent.
|
| ⊢
((φ → ψ) → ((φ → ¬ ψ) → ¬ φ)) |
| |
| Theorem | pm2.65i 116 |
Inference rulR for proof by contradiction.
|
| ⊢
(φ → ψ)
& ⊢ (φ → ¬ ψ)
⇒ ⊢ ¬ φ |
| |
| Theorem | pm2.65d 117 |
Deduction rule for proof by contradiction.
|
| ⊢
(φ → (ψ → χ))
& ⊢ (φ → (ψ → ¬ χ))
⇒ ⊢ (φ → ¬ ψ) |
| |
| Theorem | ja 118 |
Inference joining the antecedents of two premises. (The proof was
shortened by Mel L. O'Cat, 30-Aug-04.)
|
| ⊢
(¬ φ → χ)
& ⊢ (ψ → χ)
⇒ ⊢ ((φ → ψ) → χ) |
| |
| Theorem | jc 119 |
Inference joining the consequents of two premises.
|
| ⊢
(φ → ψ)
& ⊢ (φ → χ)
⇒ ⊢ (φ → ¬ (ψ → ¬ χ)) |
| |
| Theorem | pm3.26im 120 |
Simplification. Similar to Theorem *3.26 of [WhiteheadRussell] p. 112.
|
| ⊢
(¬ (φ → ¬ ψ) → φ) |
| |
| Theorem | pm3.27im 121 |
Simplification. Similar to Theorem *3.27 of [WhiteheadRussell] p. 112.
|
| ⊢
(¬ (φ → ¬ ψ) → ψ) |
| |
| Theorem | impt 122 |
Importation theorem expressed with primitive connectives.
|
| ⊢
((φ → (ψ → χ)) → (¬ (φ → ¬ ψ) → χ)) |
| |
| Theorem | expt 123 |
Exportation theorem expressed with primitive connectives.
|
| ⊢
((¬ (φ → ¬ ψ) → χ) → (φ → (ψ → χ))) |
| |
| Theorem | impi 124 |
An importation inference.
|
| ⊢
(φ → (ψ → χ))
⇒ ⊢ (¬ (φ → ¬ ψ) → χ) |
| |
| Theorem | expi 125 |
An exportation inference.
|
| ⊢
(¬ (φ → ¬ ψ) → χ)
⇒ ⊢ (φ → (ψ → χ)) |
| |
| Theorem | bijust 126 |
Theorem used to justify definition of biconditional df-bi 128. (The proof
was shortened by Josh Purinton, 29-Dec-00.)
|
| ⊢
¬ ((φ → φ) → ¬ (φ → φ)) |
| |
.TD NOWRAP>Syntax| wb 127 |
Extend our wff definition to include the biconditional connective}
|
| wff
(φ ↔ ψ) |
| |
| Definition | df-bi 128 |
This is our first definition, which defines the biconditional connective
↔. Unlike most traditional developments, we have chosen not to
have a separate symbol such as 'Df.' to mean 'is defined as.' Instead,
we will later use the biconditional connective for this purpose, as it
allows us to use logic to manipulate definitions directly (df-or 197
is
its first use). Here we use the biconditional connective to define
itself, a feat which requires a little care. We define (φ ↔ ψ)
as ¬ ((φ → ψ) → ¬ (ψ → φ)) but we don't yet have a
notation that can express this directly, so we use a more complicated
expression using the language that we have so far. The justification
for our definition is that if we mechanically substitute the second wff
for the first in the definition, the definition becomes an instance of
previously proved theorem bijust 126. Note that from Metamath's point of
view, a definition is just another axiom; but from our high level point
of view, we are are not strengthening the language since if we
mechanically eliminate the new symbol ↔ we will not end up with
any theorems we could not prove before. To indicate this fact we prefix
definition labels with "df-" instead of "ax-". (This
prefixing is an
informal convention that means nothing to the Metamath proof verifier;
it is just for human readability.) See bii 140 and
bi 396
for theorems
suggesting the typical textbook definition of ↔.
|
| ⊢
¬ (((φ ↔ ψ) → ¬ ((φ → ψ) → ¬ (ψ → φ))) → ¬ (¬ ((φ → ψ) → ¬ (ψ → φ)) → (φ ↔ ψ))) |
| |
| Theorem | biigb 129 |
This proof of bii 140, discovered by Gregory Bush on 8-Mar-04, has
several curious properties. First, it has only 17 steps directly
from the axioms and df-bi 128, compared to over 800 steps were the proof
of bii 140 expanded into axioms. Second, step 2 demands
only the property
of "true"; any axiom (or theorem) could be used. Third, it
illustrates
how intermediate steps can "blow up" in size even in short
proofs.
Fourth, the compressed proof is only 2.5 lines long, but the web page
is over 200kB in size. If there were an obfuscated code contest for
proofs, this might be a winner.
|
| ⊢
((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) |
| |
| Theorem | bi1 130 |
Property of the biconditional connective.
|
| ⊢
((φ ↔ ψ) → (φ → ψ)) |
| |
| Theorem | bi2 131 |
Property of the biconditional connective.
|
| ⊢
((φ ↔ ψ) → (ψ → φ)) |
| |
| Theorem | bi3 132 |
Property of the biconditional connective.
|
| ⊢
((φ → ψ) → ((ψ → φ) → (φ ↔ ψ))) |
| |
| Theorem | biimp 133 |
Infer an implication from a logical equivalence.
|
| ⊢
(φ ↔ ψ)
⇒ ⊢ (φ → ψ) |
| |
| Theorem | biimpr 134 |
Infer a converse implication from a logical equivalence.
|
| ⊢
(φ ↔ ψ)
⇒ ⊢ (ψ → φ) |
| |
| Theorem | biimpd 135 |
Deduce an implication from a logical equivalence.
|
| ⊢
(φ → (ψ ↔ χ))
⇒ ⊢ (φ → (ψ → χ)) |
| |
| Theorem | biimprd 136 |
Deduce a converse implication from a logical equivalence.
|
| ⊢
(φ → (ψ ↔ χ))
⇒ ⊢ (φ → (χ → ψ)) |
| |
| Theorem | biimpcd 137 |
Deduce a commuted implication from a logical equivalence.
|
| ⊢
(φ → (ψ ↔ χ))
⇒ ⊢ (ψ → (φ → χ)) |
| |
| Theorem | biimprcd 138 |
Deduce a converse commuted implication from a logical equivalence.
|
| ⊢
(φ → (ψ ↔ χ))
⇒ ⊢ (χ → (φ → ψ)) |
| |
| Theorem | impbi 139 |
Infer an equivalence from an implication and its converse.
|
| ⊢
(φ → ψ)
& ⊢ (ψ → φ)
⇒ ⊢ (φ ↔ ψ) |
| |
| Theorem | bii 140 |
Relate the biconditional connective to primitive connectives. See biigb 129
for an unusual version proved directly from axioms.
|
| ⊢
((φ ↔ ψ) ↔ ¬ ((φ → ψ) → ¬ (ψ → φ))) |
| |
| Theorem | bi2.04 141 |
Logical equivalence of commuted antecedents. Part of Theorem *4.87 of
[WhiteheadRussell] p. 122.
|
| ⊢
((φ → (ψ → χ)) ↔ (ψ → (φ → χ))) |
| |
| Theorem | pm4.13 142 |
Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117.
|
| ⊢
(φ ↔ ¬ ¬ φ) |
| |
| Theorem | pm4.1 143 |
Contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116.
|
| ⊢
((φ → ψ) ↔ (¬ ψ → ¬ φ)) |
| |
| Theorem | bi2.03 144 |
Contraposition. Bidirectional version of con2 82.
|
| ⊢
((φ → ¬ ψ) ↔ (ψ → ¬ φ)) |
| |
| Theorem | bi2.15 145 |
Contraposition. Bidirectional version of con1 84.
|
| ⊢
((¬ φ → ψ) ↔ (¬ ψ → φ)) |
| |
| Theorem | pm5.4 146 |
Antecedent absorption implication. Theorem *5.4 of
[WhiteheadRussell] p. 125.
|
| ⊢
((φ → (φ → ψ)) ↔ (φ → ψ)) |
| |
| Theorem | imdi 147 |
Distributive law for implication. Compare Theorem *5.41 of
[WhiteheadRussell] p. 125.
|
| ⊢
((φ → (ψ → χ)) ↔ ((φ → ψ) → (φ → χ))) |
| |
| Theorem | pm4.2 148 |
Principle of identity for logical equivalence. Theorem *4.2 of
[WhiteheadRussell] p. 117.
|
| ⊢
(φ ↔ φ) |
| |
| Theorem | pm4.2i 149 |
Principle of identity with antecedent.
|
| ⊢
(φ → (ψ ↔ ψ)) |
| |
| Theorem | bicomi 150 |
Inference from commutative law for logical equivalence.
|
| ⊢
(φ ↔ ψ)
⇒ ⊢ (ψ ↔ φ) |
| |
| Theorem | bitr 151 |
An inference from transitive law for logical equivalence.
|
| ⊢
(φ ↔ ψ)
& ⊢ (ψ ↔ χ)
⇒ ⊢ (φ ↔ χ) |
| |
| Theorem | bitr2 152 |
An inference from transitive law for logical equivalence.
|
| ⊢
(φ ↔ ψ)
& ⊢ (ψ ↔ χ)
⇒ ⊢ (χ ↔ φ) |
| |
| Theorem | bitr3 153 |
An inference from transitive law for logical equivalence.
|
| ⊢
(ψ ↔ φ)
& ⊢ (ψ ↔ χ)
⇒ ⊢ (φ ↔ χ) |
| |
| Theorem | bitr4 154 |
An inference from transitive law for logical equivalence.
|
| ⊢
(φ ↔ ψ)
& ⊢ (χ ↔ ψ)
⇒ ⊢ (φ ↔ χ) |
| |
| Theorem | 3bitr 155 |
A chained inference from transitive law for logical equivalence.
|
| ⊢
(φ ↔ ψ)
& ⊢ (ψ ↔ χ)
& ⊢ (χ ↔ θ)
⇒ ⊢ (φ ↔ θ) |
| |
| Theorem | 3bitr3 156 |
A chained inference from transitive law for logical equivalence.
|
| ⊢
(φ ↔ ψ)
& ⊢ (φ ↔ χ)
& ⊢ (ψ ↔ θ)
⇒ ⊢ (χ ↔ θ) |
| |
| Theorem | 3bitr3r 157 |
A chained inference from transitive law for logical equivalence.
|
| ⊢
(φ ↔ ψ)
& ⊢ (φ ↔ χ)
& ⊢ (ψ ↔ θ)
⇒ ⊢ (θ ↔ χ) |
| |
| Theorem | 3bitr4 158 |
A chained inference from transitive law for logical equivalence. This
inference is frequently used to apply a definition to both sides of a
logical equivalence.
|
| ⊢
(φ ↔ ψ)
& ⊢ (χ ↔ φ)
& ⊢ (θ ↔ ψ)
⇒ ⊢ (χ ↔ θ) |
| |
| Theorem | 3bitr4r 159 |
A chained inference from transitive law for logical equivalence.
|
| ⊢
(φ ↔ ψ)
& ⊢ (χ ↔ φ)
& ⊢ (θ ↔ ψ)
⇒ ⊢ (θ ↔ χ) |
| |
| Theorem | imbi2i 160 |
Introduce an antecedent to both sides of a logical equivalence.
|
| ⊢
(φ ↔ ψ)
⇒ ⊢ ((χ → φ) ↔ (χ → ψ)) |
| |
| Theorem | imbi1i 161 |
Introduce a consequent to both sides of a logical equivalence.
|
| ⊢
(φ ↔ ψ)
⇒ ⊢ ((φ → χ) ↔ (ψ → χ)) |
| |
| Theorem | negbii 162 |
Negate both sides of a logical equivalence.
|
| ⊢
(φ ↔ ψ)
⇒ ⊢ (¬ φ ↔ ¬ ψ) |
| |
| Theorem | imbi12i 163 |
Join two logical equivalences to form equivalence of implications.
|
| ⊢
(φ ↔ ψ)
& ⊢ (χ ↔ θ)
⇒ ⊢ ((φ → χ) ↔ (ψ → θ)) |
| |
| Theorem | mpbi 164 |
An inference from a biconditional, related to modus ponens.
|
| ⊢
φ
& ⊢ (φ ↔ ψ)
⇒ ⊢ ψ |
| |
| Theorem | mpbir 165 |
An inference from a biconditional, related to modus ponens.
|
| ⊢
ψ
& ⊢ (φ ↔ ψ)
⇒ ⊢ φ |
| |
| Theorem | mtbi 166 |
An inference from a biconditional, related to modus tollens.
|
| ⊢
¬ φ
& ⊢ (φ ↔ ψ)
⇒ ⊢ ¬ ψ |
| |
| Theorem | mtbir 167 |
An inference from a biconditional, related to modus tollens.
|
| ⊢
¬ ψ
& ⊢ (φ ↔ ψ)
⇒ ⊢ ¬ φ |
| |
| Theorem | mpbii 168 |
An inference from a nested biconditional, related to modus ponens.
|
| ⊢
ψ
& ⊢ (φ → (ψ ↔ χ))
⇒ ⊢ (φ → χ) |
| |
| Theorem | mpbiri 169 |
An inference from a nested biconditional, related to modus ponens.
|
| ⊢
χ
& ⊢ (φ → (ψ ↔ χ))
⇒ ⊢ (φ → ψ) |
| |
| Theorem | mpbid 170 |
A deduction from a biconditional, related to modus ponens.
|
| ⊢
(φ → ψ)
& ⊢ (φ → (ψ ↔ χ))
⇒ ⊢ (φ → χ) |
| |
| Theorem | mpbird 171 |
A deduction from a biconditional, related to modus ponens.
|
| ⊢
(φ → χ)
& ⊢ (φ → (ψ ↔ χ))
⇒ ⊢ (φ → ψ) |
| |
| Theorem | a1bi 172 |
Inference rule introducing a theorem as an antecedent.
|
| ⊢
φ
⇒ ⊢ (ψ ↔ (φ → ψ)) |
| |
| Theorem | sylib 173 |
A mixed syllogism inference from an implication and a biconditional.
|
| ⊢
(φ → ψ)
& ⊢ (ψ ↔ χ)
⇒ ⊢ (φ → χ) |
| |
| Theorem | sylbi 174 |
A mixed syllogism inference from a biconditional and an implication.
Useful for substituting an antecedent with a definition.
|
| ⊢
(φ ↔ ψ)
& ⊢ (ψ → χ)
⇒ ⊢ (φ → χ) |
| |
| Theorem | sylibr 175 |
A mixed syllogism inference from an implication and a biconditional.
Useful for substituting a consequent with a definition.
|
| ⊢
(φ → ψ)
& ⊢ (χ ↔ ψ)
⇒ ⊢ (φ → χ) |
| |
| Theorem | sylbir 176 |
A mixed syllogism inference from a biconditional and an implication.
|
| ⊢
(ψ ↔ φ)
& ⊢ (ψ → χ)
⇒ ⊢ (φ → χ) |
| |
| Theorem | sylibd 177 |
A syllogism deduction.
|
| ⊢
(φ → (ψ → χ))
& ⊢ (φ → (χ ↔ θ))
⇒ ⊢ (φ → (ψ → θ)) |
| |
| Theorem | sylbid 178 |
A syllogism deduction.
|
| ⊢
(φ → (ψ ↔ χ))
& ⊢ (φ → (χ → θ))
⇒ ⊢ (φ → (ψ → θ)) |
| |
| Theorem | sylibrd 179 |
A syllogism deduction.
|
| ⊢
(φ → (ψ → χ))
& ⊢ (φ → (θ ↔ χ))
⇒ ⊢ (φ → (ψ → θ)) |
| |
| Theorem | sylbird 180 |
A syllogism deduction.
|
| ⊢
(φ → (χ ↔ ψ))
& ⊢ (φ → (χ → θ))
⇒ ⊢ (φ → (ψ → θ)) |
| |
| Theorem | syl5ib 181 |
A mixed syllogism inference from a nested implication and a
biconditional. Useful for substituting an embedded antecedent with a
definition.
|
| ⊢
(φ → (ψ → χ))
& ⊢ (θ ↔ ψ)
⇒ ⊢ (φ → (θ → χ)) |
| |
| Theorem | syl5ibr 182 |
A mixed syllogism inference from a nested implication and a
biconditional.
|
| ⊢
(φ → (ψ → χ))
& ⊢ (ψ ↔ θ)
⇒ ⊢ (φ → (θ → χ)) |
| |
| Theorem | syl5bi 183 |
A mixed syllogism inference.
|
| ⊢
(φ → (ψ ↔ χ))
& ⊢ (θ → ψ)
⇒ ⊢ (φ → (θ → χ)) |
| |
| Theorem | syl5bir 184 |
A mixed syllogism inference.
|
| ⊢
(φ → (ψ ↔ χ))
& ⊢ (θ → χ)
⇒ ⊢ (φ → (θ → ψ)) |
| |
| Theorem | syl6ib 185 |
A mixed syllogism inference from a nested implication and a
biconditional.
|
| ⊢
(φ → (ψ → χ))
& ⊢ (χ ↔ θ)
⇒ ⊢ (φ → (ψ → θ)) |
| |
| Theorem | syl6ibr 186 |
A mixed syllogism inference from a nested implication and a
biconditional. Useful for substituting an embedded consequent with a
definition.
|
| ⊢
(φ → (ψ → χ))
& ⊢ (θ ↔ χ)
⇒ ⊢ (φ → (ψ → θ)) |
| |
| Theorem | syl6bi 187 |
A mixed syllogism inference.
|
| ⊢
(φ → (ψ ↔ χ))
& ⊢ (χ → θ)
⇒ ⊢ (φ → (ψ → θ)) |
| |
| Theorem | syl6bir 188 |
A mixed syllogism inference.
|
| ⊢
(φ → (χ ↔ ψ))
& ⊢ (χ → θ)
⇒ ⊢ (φ → (ψ → θ)) |
| |
| Theorem | bisyl7 189 |
A mixed syllogism inference from a doubly nested implication and a
biconditional.
|
| ⊢
(φ → (ψ → (χ → θ)))
& ⊢ (τ ↔ χ)
⇒ ⊢ (φ → (ψ → (τ → θ))) |
| |
| Theorem | bisyl8 190 |
A syllogism rule of inference. The second premise is used to replace
the consequent of the first premise.
|
| ⊢
(φ → (ψ → (χ → θ)))
& ⊢ (θ ↔ τ)
⇒ ⊢ (φ → (ψ → (χ → τ))) |
| |
| Theorem | 3imtr3 191 |
A mixed syllogism inference, useful for removing a definition from both
sides of an implication.
|
| ⊢
(φ → ψ)
& ⊢ (φ ↔ χ)
& ⊢ (ψ ↔ θ)
⇒ ⊢ (χ → θ) |
| |
| Theorem | 3imtr4 192 |
A mixed syllogism inference, useful for applying a definition to both
sides of an implication.
|
| ⊢
(φ → ψ)
& ⊢ (χ ↔ φ)
& ⊢ (θ ↔ ψ)
⇒ ⊢ (χ → θ) |
| |
| Theorem | bicon1i 193 |
A contraposition inference.
|
| ⊢
(¬ φ ↔ ψ)
⇒ ⊢ (¬ ψ ↔ φ) |
| |
| Theorem | bicon2i 194 |
A contraposition inference.
|
| ⊢
(φ ↔ ¬ ψ)
⇒ ⊢ (ψ ↔ ¬ φ) |
| |
| Syntax | wo 195 |
Extend wff definition to include disjunction ('or').
|
| wff
(φ ∨ ψ) |
| |
| Syntax | wa 196 |
Extend wff definition to include conjunction ('and').
|
| wff
(φ ∧ ψ) |
| |
| Definition | df-or 197 |
Define disjunction (logical 'or'). This is our first use of the
biconditional connective in a definition; we use it in place of the
traditional "<=def=>", which means the same thing, except
that we can
manipulate the biconditional connective directly in proofs rather than
having to rely on an informal definition substitution rule. Note that
if we mechanically substitute (¬ φ → ψ) for (φ ∨ ψ),
we end up with an instance of previously proved theorem pm4.2 148. This
is the justification for the definition, along with the fact that it
introduces a new symbol ∨. Definition of [Margaris] p. 49.
|
| ⊢
((φ ∨ ψ) ↔ (¬ φ → ψ)) |
| |
| Definition | df-an 198 |
Define conjunction (logical 'and'). Definition of [Margaris] p. 49.
|
| ⊢
((φ ∧ ψ) ↔ ¬ (φ → ¬ ψ)) |
| |
| Theorem | dfor2 199 |
Logical 'or' expressed in terms of implication only. Theorem *5.25 of
[WhiteheadRussell] p. 124.
|
| ⊢
((φ ∨ ψ) ↔ ((φ → ψ) → ψ)) |
| |
| Theorem | ori 200 |
Inference from disjunction definition.
|
| ⊢
(φ ∨ ψ)
⇒ ⊢ (¬ φ → ψ) |
Home
Hilbert Space Explorer
(4958-5787)