Theorem List for Intuitionistic Logic Explorer - 601-700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | bianabs 601 |
Absorb a hypothesis into the second member of a biconditional.
(Contributed by FL, 15-Feb-2007.)
|
⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
|
Theorem | biadani 602 |
An implication implies to the equivalence of some implied equivalence
and some other equivalence involving a conjunction. (Contributed by BJ,
4-Mar-2023.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜓 → (𝜑 ↔ 𝜒)) ↔ (𝜑 ↔ (𝜓 ∧ 𝜒))) |
|
Theorem | biadanii 603 |
Inference associated with biadani 602. Add a conjunction to an
equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof
shortened by BJ, 4-Mar-2023.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜓 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) |
|
1.2.5 Logical negation
(intuitionistic)
|
|
Axiom | ax-in1 604 |
'Not' introduction. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.) Use its alias pm2.01 606
instead. (New usage is discouraged.)
|
⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑) |
|
Axiom | ax-in2 605 |
'Not' elimination. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.)
|
⊢ (¬ 𝜑 → (𝜑 → 𝜓)) |
|
Theorem | pm2.01 606 |
Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. This
is valid intuitionistically (in the terminology of Section 1.2 of [Bauer]
p. 482 it is a proof of negation not a proof by contradiction); compare
with pm2.18dc 841 which only holds for some propositions. Also
called weak
Clavius law. (Contributed by Mario Carneiro, 12-May-2015.)
|
⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑) |
|
Theorem | pm2.21 607 |
From a wff and its negation, anything is true. Theorem *2.21 of
[WhiteheadRussell] p. 104. Also
called the Duns Scotus law. (Contributed
by Mario Carneiro, 12-May-2015.)
|
⊢ (¬ 𝜑 → (𝜑 → 𝜓)) |
|
Theorem | pm2.01d 608 |
Deduction based on reductio ad absurdum. (Contributed by NM,
18-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ (𝜑 → (𝜓 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | pm2.21d 609 |
A contradiction implies anything. Deduction from pm2.21 607.
(Contributed by NM, 10-Feb-1996.)
|
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) |
|
Theorem | pm2.21dd 610 |
A contradiction implies anything. Deduction from pm2.21 607.
(Contributed by Mario Carneiro, 9-Feb-2017.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | pm2.24 611 |
Theorem *2.24 of [WhiteheadRussell] p.
104. (Contributed by NM,
3-Jan-2005.)
|
⊢ (𝜑 → (¬ 𝜑 → 𝜓)) |
|
Theorem | pm2.24d 612 |
Deduction version of pm2.24 611. (Contributed by NM, 30-Jan-2006.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
|
Theorem | pm2.24i 613 |
Inference version of pm2.24 611. (Contributed by NM, 20-Aug-2001.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ 𝜑 ⇒ ⊢ (¬ 𝜑 → 𝜓) |
|
Theorem | con2d 614 |
A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised
by NM, 12-Feb-2013.)
|
⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → ¬ 𝜓)) |
|
Theorem | mt2d 615 |
Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
|
⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | nsyl3 616 |
A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
(Revised by NM, 13-Jun-2013.)
|
⊢ (𝜑 → ¬ 𝜓)
& ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜒 → ¬ 𝜑) |
|
Theorem | con2i 617 |
A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen,
13-Jun-2013.)
|
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜓 → ¬ 𝜑) |
|
Theorem | nsyl 618 |
A negated syllogism inference. (Contributed by NM, 31-Dec-1993.)
(Proof shortened by Wolf Lammen, 2-Mar-2013.)
|
⊢ (𝜑 → ¬ 𝜓)
& ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜒) |
|
Theorem | notnot 619 |
Double negation introduction. Theorem *2.12 of [WhiteheadRussell] p. 101.
The converse need not hold. It holds exactly for stable propositions (by
definition, see df-stab 817) and in particular for decidable propositions
(see notnotrdc 829). See also notnotnot 624. (Contributed by NM,
28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
|
⊢ (𝜑 → ¬ ¬ 𝜑) |
|
Theorem | notnotd 620 |
Deduction associated with notnot 619 and notnoti 635. (Contributed by
Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf
Lammen, 27-Mar-2021.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ¬ ¬ 𝜓) |
|
Theorem | con3d 621 |
A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised
by NM, 31-Jan-2015.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
|
Theorem | con3i 622 |
A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by Wolf Lammen, 20-Jun-2013.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (¬ 𝜓 → ¬ 𝜑) |
|
Theorem | con3rr3 623 |
Rotate through consequent right. (Contributed by Wolf Lammen,
3-Nov-2013.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (¬ 𝜒 → (𝜑 → ¬ 𝜓)) |
|
Theorem | notnotnot 624 |
Triple negation is equivalent to negation. (Contributed by Jim Kingdon,
28-Jul-2018.)
|
⊢ (¬ ¬ ¬ 𝜑 ↔ ¬ 𝜑) |
|
Theorem | con3dimp 625 |
Variant of con3d 621 with importation. (Contributed by Jonathan
Ben-Naim,
3-Jun-2011.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓) |
|
Theorem | pm2.01da 626 |
Deduction based on reductio ad absurdum. (Contributed by Mario
Carneiro, 9-Feb-2017.)
|
⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | pm3.2im 627 |
In classical logic, this is just a restatement of pm3.2 138. In
intuitionistic logic, it still holds, but is weaker than pm3.2.
(Contributed by Mario Carneiro, 12-May-2015.)
|
⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓))) |
|
Theorem | expi 628 |
An exportation inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by O'Cat, 28-Nov-2008.)
|
⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) |
|
Theorem | pm2.65i 629 |
Inference for proof by contradiction. (Contributed by NM, 18-May-1994.)
(Proof shortened by Wolf Lammen, 11-Sep-2013.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ ¬ 𝜑 |
|
Theorem | mt2 630 |
A rule similar to modus tollens. (Contributed by NM, 19-Aug-1993.)
(Proof shortened by Wolf Lammen, 10-Sep-2013.)
|
⊢ 𝜓
& ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ ¬ 𝜑 |
|
Theorem | biijust 631 |
Theorem used to justify definition of intuitionistic biconditional
df-bi 116. (Contributed by NM, 24-Nov-2017.)
|
⊢ ((((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))) |
|
Theorem | con3 632 |
Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed
by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)
|
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) |
|
Theorem | con2 633 |
Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed
by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
|
⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑)) |
|
Theorem | mt2i 634 |
Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof
shortened by Wolf Lammen, 15-Sep-2012.)
|
⊢ 𝜒
& ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | notnoti 635 |
Infer double negation. (Contributed by NM, 27-Feb-2008.)
|
⊢ 𝜑 ⇒ ⊢ ¬ ¬ 𝜑 |
|
Theorem | pm2.21i 636 |
A contradiction implies anything. Inference from pm2.21 607.
(Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
⊢ ¬ 𝜑 ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | pm2.24ii 637 |
A contradiction implies anything. Inference from pm2.24 611.
(Contributed by NM, 27-Feb-2008.)
|
⊢ 𝜑
& ⊢ ¬ 𝜑 ⇒ ⊢ 𝜓 |
|
Theorem | nsyld 638 |
A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.)
|
⊢ (𝜑 → (𝜓 → ¬ 𝜒)) & ⊢ (𝜑 → (𝜏 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ¬ 𝜏)) |
|
Theorem | nsyli 639 |
A negated syllogism inference. (Contributed by NM, 3-May-1994.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → ¬ 𝜒) ⇒ ⊢ (𝜑 → (𝜃 → ¬ 𝜓)) |
|
Theorem | jc 640 |
Inference joining the consequents of two premises. (Contributed by NM,
5-Aug-1993.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → ¬ (𝜓 → ¬ 𝜒)) |
|
Theorem | jcn 641 |
Theorem joining the consequents of two premises. Theorem 8 of [Margaris]
p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh
Purinton, 29-Dec-2000.)
|
⊢ (𝜑 → (¬ 𝜓 → ¬ (𝜑 → 𝜓))) |
|
Theorem | jcnd 642 |
Deduction joining the consequents of two premises. (Contributed by
Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen,
10-Apr-2024.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → ¬ (𝜓 → 𝜒)) |
|
Theorem | conax1 643 |
Contrapositive of ax-1 6. (Contributed by BJ, 28-Oct-2023.)
|
⊢ (¬ (𝜑 → 𝜓) → ¬ 𝜓) |
|
Theorem | conax1k 644 |
Weakening of conax1 643. General instance of pm2.51 645 and of pm2.52 646.
(Contributed by BJ, 28-Oct-2023.)
|
⊢ (¬ (𝜑 → 𝜓) → (𝜒 → ¬ 𝜓)) |
|
Theorem | pm2.51 645 |
Theorem *2.51 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
⊢ (¬ (𝜑 → 𝜓) → (𝜑 → ¬ 𝜓)) |
|
Theorem | pm2.52 646 |
Theorem *2.52 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → ¬ 𝜓)) |
|
Theorem | expt 647 |
Exportation theorem pm3.3 259 (closed form of ex 114)
expressed with
primitive connectives. (Contributed by NM, 5-Aug-1993.)
|
⊢ ((¬ (𝜑 → ¬ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) |
|
Theorem | jarl 648 |
Elimination of a nested antecedent. (Contributed by Wolf Lammen,
10-May-2013.)
|
⊢ (((𝜑 → 𝜓) → 𝜒) → (¬ 𝜑 → 𝜒)) |
|
Theorem | pm2.65 649 |
Theorem *2.65 of [WhiteheadRussell] p.
107. Proof by contradiction.
Proofs, such as this one, which assume a proposition, here 𝜑, derive
a contradiction, and therefore conclude ¬ 𝜑, are valid
intuitionistically (and can be called "proof of negation", for
example by
Section 1.2 of [Bauer] p. 482). By
contrast, proofs which assume
¬ 𝜑, derive a contradiction, and
conclude 𝜑, such as
condandc 867, are only valid for decidable propositions.
(Contributed by
NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Mar-2013.)
|
⊢ ((𝜑 → 𝜓) → ((𝜑 → ¬ 𝜓) → ¬ 𝜑)) |
|
Theorem | pm2.65d 650 |
Deduction for proof by contradiction. (Contributed by NM, 26-Jun-1994.)
(Proof shortened by Wolf Lammen, 26-May-2013.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | pm2.65da 651 |
Deduction for proof by contradiction. (Contributed by NM,
12-Jun-2014.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒)
& ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | mto 652 |
The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof
shortened by Wolf Lammen, 11-Sep-2013.)
|
⊢ ¬ 𝜓
& ⊢ (𝜑 → 𝜓) ⇒ ⊢ ¬ 𝜑 |
|
Theorem | mtod 653 |
Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof
shortened by Wolf Lammen, 11-Sep-2013.)
|
⊢ (𝜑 → ¬ 𝜒)
& ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | mtoi 654 |
Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof
shortened by Wolf Lammen, 15-Sep-2012.)
|
⊢ ¬ 𝜒
& ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | mtand 655 |
A modus tollens deduction. (Contributed by Jeff Hankins,
19-Aug-2009.)
|
⊢ (𝜑 → ¬ 𝜒)
& ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | notbi 656 |
Equivalence property for negation. Closed form. (Contributed by BJ,
27-Jan-2020.)
|
⊢ ((𝜑 ↔ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓)) |
|
Theorem | notbid 657 |
Equivalence property for negation. Deduction form. (Contributed by NM,
21-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) |
|
Theorem | notbii 658 |
Equivalence property for negation. Inference form. (Contributed by NM,
5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (¬ 𝜑 ↔ ¬ 𝜓) |
|
Theorem | con2b 659 |
Contraposition. Bidirectional version of con2 633.
(Contributed by NM,
5-Aug-1993.)
|
⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑)) |
|
Theorem | mtbi 660 |
An inference from a biconditional, related to modus tollens.
(Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen,
25-Oct-2012.)
|
⊢ ¬ 𝜑
& ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ¬ 𝜓 |
|
Theorem | mtbir 661 |
An inference from a biconditional, related to modus tollens.
(Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen,
14-Oct-2012.)
|
⊢ ¬ 𝜓
& ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ¬ 𝜑 |
|
Theorem | mtbid 662 |
A deduction from a biconditional, similar to modus tollens.
(Contributed by NM, 26-Nov-1995.)
|
⊢ (𝜑 → ¬ 𝜓)
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) |
|
Theorem | mtbird 663 |
A deduction from a biconditional, similar to modus tollens.
(Contributed by NM, 10-May-1994.)
|
⊢ (𝜑 → ¬ 𝜒)
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | mtbii 664 |
An inference from a biconditional, similar to modus tollens.
(Contributed by NM, 27-Nov-1995.)
|
⊢ ¬ 𝜓
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) |
|
Theorem | mtbiri 665 |
An inference from a biconditional, similar to modus tollens.
(Contributed by NM, 24-Aug-1995.)
|
⊢ ¬ 𝜒
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | sylnib 666 |
A mixed syllogism inference from an implication and a biconditional.
(Contributed by Wolf Lammen, 16-Dec-2013.)
|
⊢ (𝜑 → ¬ 𝜓)
& ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 → ¬ 𝜒) |
|
Theorem | sylnibr 667 |
A mixed syllogism inference from an implication and a biconditional.
Useful for substituting an consequent with a definition. (Contributed
by Wolf Lammen, 16-Dec-2013.)
|
⊢ (𝜑 → ¬ 𝜓)
& ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜒) |
|
Theorem | sylnbi 668 |
A mixed syllogism inference from a biconditional and an implication.
Useful for substituting an antecedent with a definition. (Contributed
by Wolf Lammen, 16-Dec-2013.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ (¬ 𝜓 → 𝜒) ⇒ ⊢ (¬ 𝜑 → 𝜒) |
|
Theorem | sylnbir 669 |
A mixed syllogism inference from a biconditional and an implication.
(Contributed by Wolf Lammen, 16-Dec-2013.)
|
⊢ (𝜓 ↔ 𝜑)
& ⊢ (¬ 𝜓 → 𝜒) ⇒ ⊢ (¬ 𝜑 → 𝜒) |
|
Theorem | xchnxbi 670 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
⊢ (¬ 𝜑 ↔ 𝜓)
& ⊢ (𝜑 ↔ 𝜒) ⇒ ⊢ (¬ 𝜒 ↔ 𝜓) |
|
Theorem | xchnxbir 671 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
⊢ (¬ 𝜑 ↔ 𝜓)
& ⊢ (𝜒 ↔ 𝜑) ⇒ ⊢ (¬ 𝜒 ↔ 𝜓) |
|
Theorem | xchbinx 672 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
⊢ (𝜑 ↔ ¬ 𝜓)
& ⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (𝜑 ↔ ¬ 𝜒) |
|
Theorem | xchbinxr 673 |
Replacement of a subexpression by an equivalent one. (Contributed by
Wolf Lammen, 27-Sep-2014.)
|
⊢ (𝜑 ↔ ¬ 𝜓)
& ⊢ (𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ ¬ 𝜒) |
|
Theorem | mt2bi 674 |
A false consequent falsifies an antecedent. (Contributed by NM,
19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
|
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 ↔ (𝜓 → ¬ 𝜑)) |
|
Theorem | mtt 675 |
Modus-tollens-like theorem. (Contributed by NM, 7-Apr-2001.) (Revised by
Mario Carneiro, 31-Jan-2015.)
|
⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜓 → 𝜑))) |
|
Theorem | annimim 676 |
Express conjunction in terms of implication. One direction of Theorem
*4.61 of [WhiteheadRussell] p.
120. The converse holds for decidable
propositions, as can be seen at annimdc 922. (Contributed by Jim Kingdon,
24-Dec-2017.)
|
⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ (𝜑 → 𝜓)) |
|
Theorem | pm4.65r 677 |
One direction of Theorem *4.65 of [WhiteheadRussell] p. 120. The converse
holds in classical logic. (Contributed by Jim Kingdon, 28-Jul-2018.)
|
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ¬ (¬ 𝜑 → 𝜓)) |
|
Theorem | imanim 678 |
Express implication in terms of conjunction. The converse only holds
given a decidability condition; see imandc 875. (Contributed by Jim
Kingdon, 24-Dec-2017.)
|
⊢ ((𝜑 → 𝜓) → ¬ (𝜑 ∧ ¬ 𝜓)) |
|
Theorem | pm3.37 679 |
Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112. (Contributed
by NM,
3-Jan-2005.)
|
⊢ (((𝜑 ∧ 𝜓) → 𝜒) → ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓)) |
|
Theorem | imnan 680 |
Express implication in terms of conjunction. (Contributed by NM,
9-Apr-1994.) (Revised by Mario Carneiro, 1-Feb-2015.)
|
⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) |
|
Theorem | imnani 681 |
Express implication in terms of conjunction. (Contributed by Mario
Carneiro, 28-Sep-2015.)
|
⊢ ¬ (𝜑 ∧ 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | nan 682 |
Theorem to move a conjunct in and out of a negation. (Contributed by NM,
9-Nov-2003.)
|
⊢ ((𝜑 → ¬ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) → ¬ 𝜒)) |
|
Theorem | pm3.24 683 |
Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who
call it the "law of contradiction"). (Contributed by NM,
16-Sep-1993.)
(Revised by Mario Carneiro, 2-Feb-2015.)
|
⊢ ¬ (𝜑 ∧ ¬ 𝜑) |
|
Theorem | pm4.15 684 |
Theorem *4.15 of [WhiteheadRussell] p.
117. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
|
⊢ (((𝜑 ∧ 𝜓) → ¬ 𝜒) ↔ ((𝜓 ∧ 𝜒) → ¬ 𝜑)) |
|
Theorem | pm5.21 685 |
Two propositions are equivalent if they are both false. Theorem *5.21 of
[WhiteheadRussell] p. 124.
(Contributed by NM, 21-May-1994.) (Revised by
Mario Carneiro, 31-Jan-2015.)
|
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → (𝜑 ↔ 𝜓)) |
|
Theorem | pm5.21im 686 |
Two propositions are equivalent if they are both false. Closed form of
2false 691. Equivalent to a biimpr 129-like version of the xor-connective.
(Contributed by Wolf Lammen, 13-May-2013.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
⊢ (¬ 𝜑 → (¬ 𝜓 → (𝜑 ↔ 𝜓))) |
|
Theorem | nbn2 687 |
The negation of a wff is equivalent to the wff's equivalence to falsehood.
(Contributed by Juha Arpiainen, 19-Jan-2006.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
⊢ (¬ 𝜑 → (¬ 𝜓 ↔ (𝜑 ↔ 𝜓))) |
|
Theorem | bibif 688 |
Transfer negation via an equivalence. (Contributed by NM, 3-Oct-2007.)
(Proof shortened by Wolf Lammen, 28-Jan-2013.)
|
⊢ (¬ 𝜓 → ((𝜑 ↔ 𝜓) ↔ ¬ 𝜑)) |
|
Theorem | nbn 689 |
The negation of a wff is equivalent to the wff's equivalence to
falsehood. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf
Lammen, 3-Oct-2013.)
|
⊢ ¬ 𝜑 ⇒ ⊢ (¬ 𝜓 ↔ (𝜓 ↔ 𝜑)) |
|
Theorem | nbn3 690 |
Transfer falsehood via equivalence. (Contributed by NM,
11-Sep-2006.)
|
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 ↔ (𝜓 ↔ ¬ 𝜑)) |
|
Theorem | 2false 691 |
Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ ¬ 𝜑
& ⊢ ¬ 𝜓 ⇒ ⊢ (𝜑 ↔ 𝜓) |
|
Theorem | 2falsed 692 |
Two falsehoods are equivalent (deduction form). (Contributed by NM,
11-Oct-2013.)
|
⊢ (𝜑 → ¬ 𝜓)
& ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
|
Theorem | pm5.21ni 693 |
Two propositions implying a false one are equivalent. (Contributed by
NM, 16-Feb-1996.) (Proof shortened by Wolf Lammen, 19-May-2013.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜒 → 𝜓) ⇒ ⊢ (¬ 𝜓 → (𝜑 ↔ 𝜒)) |
|
Theorem | pm5.21nii 694 |
Eliminate an antecedent implied by each side of a biconditional.
(Contributed by NM, 21-May-1999.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜒 → 𝜓)
& ⊢ (𝜓 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜒) |
|
Theorem | pm5.21ndd 695 |
Eliminate an antecedent implied by each side of a biconditional,
deduction version. (Contributed by Paul Chapman, 21-Nov-2012.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ (𝜑 → (𝜒 → 𝜓)) & ⊢ (𝜑 → (𝜃 → 𝜓)) & ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) ⇒ ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
|
Theorem | pm5.19 696 |
Theorem *5.19 of [WhiteheadRussell] p.
124. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ ¬ (𝜑 ↔ ¬ 𝜑) |
|
Theorem | pm4.8 697 |
Theorem *4.8 of [WhiteheadRussell] p.
122. This one holds for all
propositions, but compare with pm4.81dc 894 which requires a decidability
condition. (Contributed by NM, 3-Jan-2005.)
|
⊢ ((𝜑 → ¬ 𝜑) ↔ ¬ 𝜑) |
|
1.2.6 Logical disjunction
|
|
Syntax | wo 698 |
Extend wff definition to include disjunction ('or').
|
wff (𝜑 ∨ 𝜓) |
|
Axiom | ax-io 699 |
Definition of 'or'. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.) Use its alias jaob 700
instead. (New usage is discouraged.)
|
⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓))) |
|
Theorem | jaob 700 |
Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell]
p. 121. Alias of ax-io 699. (Contributed by NM, 30-May-1994.) (Revised
by Mario Carneiro, 31-Jan-2015.)
|
⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓))) |