Theorem List for Intuitionistic Logic Explorer - 501-600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | an13s 501 |
Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑)) → 𝜃) |
|
Theorem | an32s 502 |
Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) |
|
Theorem | ancom1s 503 |
Inference commuting a nested conjunction in antecedent. (Contributed by
NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃) |
|
Theorem | an31s 504 |
Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜒 ∧ 𝜓) ∧ 𝜑) → 𝜃) |
|
Theorem | anass1rs 505 |
Commutative-associative law for conjunction in an antecedent.
(Contributed by Jeff Madsen, 19-Jun-2011.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) |
|
Theorem | anabs1 506 |
Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.)
(Proof shortened by Wolf Lammen, 16-Nov-2013.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) ↔ (𝜑 ∧ 𝜓)) |
|
Theorem | anabs5 507 |
Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.)
(Proof shortened by Wolf Lammen, 9-Dec-2012.)
|
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓)) |
|
Theorem | anabs7 508 |
Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.)
(Proof shortened by Wolf Lammen, 17-Nov-2013.)
|
⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓)) |
|
Theorem | anabsan 509 |
Absorption of antecedent with conjunction. (Contributed by NM,
24-Mar-1996.) (Revised by NM, 18-Nov-2013.)
|
⊢ (((𝜑 ∧ 𝜑) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabss1 510 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabss4 511 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.)
|
⊢ (((𝜓 ∧ 𝜑) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabss5 512 |
Absorption of antecedent into conjunction. (Contributed by NM,
10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
|
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabsi5 513 |
Absorption of antecedent into conjunction. (Contributed by NM,
11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
|
⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabsi6 514 |
Absorption of antecedent into conjunction. (Contributed by NM,
14-Aug-2000.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜑) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabsi7 515 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
|
⊢ (𝜓 → ((𝜑 ∧ 𝜓) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabsi8 516 |
Absorption of antecedent into conjunction. (Contributed by NM,
26-Sep-1999.)
|
⊢ (𝜓 → ((𝜓 ∧ 𝜑) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabss7 517 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 19-Nov-2013.)
|
⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabsan2 518 |
Absorption of antecedent with conjunction. (Contributed by NM,
10-May-2004.) (Revised by NM, 1-Jan-2013.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabss3 519 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | an4 520 |
Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃))) |
|
Theorem | an42 521 |
Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓))) |
|
Theorem | an4s 522 |
Inference rearranging 4 conjuncts in antecedent. (Contributed by NM,
10-Aug-1995.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
|
Theorem | an42s 523 |
Inference rearranging 4 conjuncts in antecedent. (Contributed by NM,
10-Aug-1995.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏) |
|
Theorem | anandi 524 |
Distribution of conjunction over conjunction. (Contributed by NM,
14-Aug-1995.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) |
|
Theorem | anandir 525 |
Distribution of conjunction over conjunction. (Contributed by NM,
24-Aug-1995.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒))) |
|
Theorem | anandis 526 |
Inference that undistributes conjunction in the antecedent.
(Contributed by NM, 7-Jun-2004.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏) |
|
Theorem | anandirs 527 |
Inference that undistributes conjunction in the antecedent.
(Contributed by NM, 7-Jun-2004.)
|
⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜏) |
|
Theorem | impbida 528 |
Deduce an equivalence from two implications. (Contributed by NM,
17-Feb-2007.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒)
& ⊢ ((𝜑 ∧ 𝜒) → 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
|
Theorem | pm3.45 529 |
Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed
by NM,
3-Jan-2005.)
|
⊢ ((𝜑 → 𝜓) → ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))) |
|
Theorem | im2anan9 530 |
Deduction joining nested implications to form implication of
conjunctions. (Contributed by NM, 29-Feb-1996.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂))) |
|
Theorem | im2anan9r 531 |
Deduction joining nested implications to form implication of
conjunctions. (Contributed by NM, 29-Feb-1996.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂))) |
|
Theorem | anim12dan 532 |
Conjoin antecedents and consequents in a deduction. (Contributed by
Mario Carneiro, 12-May-2014.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒)
& ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏)) |
|
Theorem | pm5.1 533 |
Two propositions are equivalent if they are both true. Theorem *5.1 of
[WhiteheadRussell] p. 123.
(Contributed by NM, 21-May-1994.)
|
⊢ ((𝜑 ∧ 𝜓) → (𝜑 ↔ 𝜓)) |
|
Theorem | pm3.43 534 |
Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed
by NM,
3-Jan-2005.) (Revised by NM, 27-Nov-2013.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∧ 𝜒))) |
|
Theorem | jcab 535 |
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.)
|
⊢ ((𝜑 → (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒))) |
|
Theorem | pm4.76 536 |
Theorem *4.76 of [WhiteheadRussell] p.
121. (Contributed by NM,
3-Jan-2005.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒))) |
|
Theorem | pm4.38 537 |
Theorem *4.38 of [WhiteheadRussell] p.
118. (Contributed by NM,
3-Jan-2005.)
|
⊢ (((𝜑 ↔ 𝜒) ∧ (𝜓 ↔ 𝜃)) → ((𝜑 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃))) |
|
Theorem | bi2anan9 538 |
Deduction joining two equivalences to form equivalence of conjunctions.
(Contributed by NM, 31-Jul-1995.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜏 ↔ 𝜂)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
|
Theorem | bi2anan9r 539 |
Deduction joining two equivalences to form equivalence of conjunctions.
(Contributed by NM, 19-Feb-1996.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜏 ↔ 𝜂)) ⇒ ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
|
Theorem | bi2bian9 540 |
Deduction joining two biconditionals with different antecedents.
(Contributed by NM, 12-May-2004.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜏 ↔ 𝜂)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ↔ 𝜏) ↔ (𝜒 ↔ 𝜂))) |
|
Theorem | pm5.33 541 |
Theorem *5.33 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
⊢ ((𝜑 ∧ (𝜓 → 𝜒)) ↔ (𝜑 ∧ ((𝜑 ∧ 𝜓) → 𝜒))) |
|
Theorem | pm5.36 542 |
Theorem *5.36 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
⊢ ((𝜑 ∧ (𝜑 ↔ 𝜓)) ↔ (𝜓 ∧ (𝜑 ↔ 𝜓))) |
|
Theorem | bianabs 543 |
Absorb a hypothesis into the second member of a biconditional.
(Contributed by FL, 15-Feb-2007.)
|
⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
|
1.2.5 Logical negation
(intuitionistic)
|
|
Axiom | ax-in1 544 |
'Not' introduction. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.)
|
⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑) |
|
Axiom | ax-in2 545 |
'Not' elimination. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.)
|
⊢ (¬ 𝜑 → (𝜑 → 𝜓)) |
|
Theorem | pm2.01 546 |
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 750 which only holds for some propositions.
(Contributed by
Mario Carneiro, 12-May-2015.)
|
⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑) |
|
Theorem | pm2.21 547 |
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 548 |
Deduction based on reductio ad absurdum. (Contributed by NM,
18-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ (𝜑 → (𝜓 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | pm2.21d 549 |
A contradiction implies anything. Deduction from pm2.21 547.
(Contributed by NM, 10-Feb-1996.)
|
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) |
|
Theorem | pm2.21dd 550 |
A contradiction implies anything. Deduction from pm2.21 547.
(Contributed by Mario Carneiro, 9-Feb-2017.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | pm2.24 551 |
Theorem *2.24 of [WhiteheadRussell] p.
104. (Contributed by NM,
3-Jan-2005.)
|
⊢ (𝜑 → (¬ 𝜑 → 𝜓)) |
|
Theorem | pm2.24d 552 |
Deduction version of pm2.24 551. (Contributed by NM, 30-Jan-2006.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
|
Theorem | pm2.24i 553 |
Inference version of pm2.24 551. (Contributed by NM, 20-Aug-2001.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ 𝜑 ⇒ ⊢ (¬ 𝜑 → 𝜓) |
|
Theorem | con2d 554 |
A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised
by NM, 12-Feb-2013.)
|
⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → ¬ 𝜓)) |
|
Theorem | mt2d 555 |
Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
|
⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | nsyl3 556 |
A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
(Revised by NM, 13-Jun-2013.)
|
⊢ (𝜑 → ¬ 𝜓)
& ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜒 → ¬ 𝜑) |
|
Theorem | con2i 557 |
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 558 |
A negated syllogism inference. (Contributed by NM, 31-Dec-1993.)
(Proof shortened by Wolf Lammen, 2-Mar-2013.)
|
⊢ (𝜑 → ¬ 𝜓)
& ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜒) |
|
Theorem | notnot 559 |
Double negation introduction. Theorem *2.12 of [WhiteheadRussell] p. 101.
This one holds for all propositions, but its converse only holds for
decidable propositions (see notnotrdc 751). (Contributed by NM,
28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
|
⊢ (𝜑 → ¬ ¬ 𝜑) |
|
Theorem | notnotd 560 |
Deduction associated with notnot 559 and notnoti 574. (Contributed by
Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf
Lammen, 27-Mar-2021.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ¬ ¬ 𝜓) |
|
Theorem | con3d 561 |
A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised
by NM, 31-Jan-2015.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
|
Theorem | con3i 562 |
A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by Wolf Lammen, 20-Jun-2013.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (¬ 𝜓 → ¬ 𝜑) |
|
Theorem | con3rr3 563 |
Rotate through consequent right. (Contributed by Wolf Lammen,
3-Nov-2013.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (¬ 𝜒 → (𝜑 → ¬ 𝜓)) |
|
Theorem | con3and 564 |
Variant of con3d 561 with importation. (Contributed by Jonathan
Ben-Naim,
3-Jun-2011.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓) |
|
Theorem | pm2.01da 565 |
Deduction based on reductio ad absurdum. (Contributed by Mario
Carneiro, 9-Feb-2017.)
|
⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | pm3.2im 566 |
In classical logic, this is just a restatement of pm3.2 126. In
intuitionistic logic, it still holds, but is weaker than pm3.2.
(Contributed by Mario Carneiro, 12-May-2015.)
|
⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓))) |
|
Theorem | expi 567 |
An exportation inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by O'Cat, 28-Nov-2008.)
|
⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) |
|
Theorem | pm2.65i 568 |
Inference rule for proof by contradiction. (Contributed by NM,
18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ ¬ 𝜑 |
|
Theorem | mt2 569 |
A rule similar to modus tollens. (Contributed by NM, 19-Aug-1993.)
(Proof shortened by Wolf Lammen, 10-Sep-2013.)
|
⊢ 𝜓
& ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ ¬ 𝜑 |
|
Theorem | biijust 570 |
Theorem used to justify definition of intuitionistic biconditional
df-bi 110. (Contributed by NM, 24-Nov-2017.)
|
⊢ ((((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))) |
|
Theorem | con3 571 |
Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed
by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)
|
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) |
|
Theorem | con2 572 |
Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed
by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
|
⊢ ((𝜑 → ¬ 𝜓) → (𝜓 → ¬ 𝜑)) |
|
Theorem | mt2i 573 |
Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof
shortened by Wolf Lammen, 15-Sep-2012.)
|
⊢ 𝜒
& ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | notnoti 574 |
Infer double negation. (Contributed by NM, 27-Feb-2008.)
|
⊢ 𝜑 ⇒ ⊢ ¬ ¬ 𝜑 |
|
Theorem | pm2.21i 575 |
A contradiction implies anything. Inference from pm2.21 547.
(Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro,
31-Jan-2015.)
|
⊢ ¬ 𝜑 ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | pm2.24ii 576 |
A contradiction implies anything. Inference from pm2.24 551.
(Contributed by NM, 27-Feb-2008.)
|
⊢ 𝜑
& ⊢ ¬ 𝜑 ⇒ ⊢ 𝜓 |
|
Theorem | nsyld 577 |
A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.)
|
⊢ (𝜑 → (𝜓 → ¬ 𝜒)) & ⊢ (𝜑 → (𝜏 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ¬ 𝜏)) |
|
Theorem | nsyli 578 |
A negated syllogism inference. (Contributed by NM, 3-May-1994.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → ¬ 𝜒) ⇒ ⊢ (𝜑 → (𝜃 → ¬ 𝜓)) |
|
Theorem | mth8 579 |
Theorem 8 of [Margaris] p. 60. (Contributed
by NM, 5-Aug-1993.) (Proof
shortened by Josh Purinton, 29-Dec-2000.)
|
⊢ (𝜑 → (¬ 𝜓 → ¬ (𝜑 → 𝜓))) |
|
Theorem | jc 580 |
Inference joining the consequents of two premises. (Contributed by NM,
5-Aug-1993.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → ¬ (𝜓 → ¬ 𝜒)) |
|
Theorem | pm2.51 581 |
Theorem *2.51 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.)
|
⊢ (¬ (𝜑 → 𝜓) → (𝜑 → ¬ 𝜓)) |
|
Theorem | pm2.52 582 |
Theorem *2.52 of [WhiteheadRussell] p.
107. (Contributed by NM,
3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ (¬ (𝜑 → 𝜓) → (¬ 𝜑 → ¬ 𝜓)) |
|
Theorem | expt 583 |
Exportation theorem expressed with primitive connectives. (Contributed by
NM, 5-Aug-1993.)
|
⊢ ((¬ (𝜑 → ¬ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) |
|
Theorem | jarl 584 |
Elimination of a nested antecedent. (Contributed by Wolf Lammen,
10-May-2013.)
|
⊢ (((𝜑 → 𝜓) → 𝜒) → (¬ 𝜑 → 𝜒)) |
|
Theorem | pm2.65 585 |
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 775, are only valid for decidable propositions.
(Contributed by
NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Mar-2013.)
|
⊢ ((𝜑 → 𝜓) → ((𝜑 → ¬ 𝜓) → ¬ 𝜑)) |
|
Theorem | pm2.65d 586 |
Deduction rule for proof by contradiction. (Contributed by NM,
26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | pm2.65da 587 |
Deduction rule for proof by contradiction. (Contributed by NM,
12-Jun-2014.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒)
& ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | mto 588 |
The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof
shortened by Wolf Lammen, 11-Sep-2013.)
|
⊢ ¬ 𝜓
& ⊢ (𝜑 → 𝜓) ⇒ ⊢ ¬ 𝜑 |
|
Theorem | mtod 589 |
Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof
shortened by Wolf Lammen, 11-Sep-2013.)
|
⊢ (𝜑 → ¬ 𝜒)
& ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | mtoi 590 |
Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof
shortened by Wolf Lammen, 15-Sep-2012.)
|
⊢ ¬ 𝜒
& ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | mtand 591 |
A modus tollens deduction. (Contributed by Jeff Hankins,
19-Aug-2009.)
|
⊢ (𝜑 → ¬ 𝜒)
& ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | notbid 592 |
Deduction negating both sides of a logical equivalence. (Contributed by
NM, 21-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒)) |
|
Theorem | con2b 593 |
Contraposition. Bidirectional version of con2 572.
(Contributed by NM,
5-Aug-1993.)
|
⊢ ((𝜑 → ¬ 𝜓) ↔ (𝜓 → ¬ 𝜑)) |
|
Theorem | notbii 594 |
Negate both sides of a logical equivalence. (Contributed by NM,
5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (¬ 𝜑 ↔ ¬ 𝜓) |
|
Theorem | mtbi 595 |
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 596 |
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 597 |
A deduction from a biconditional, similar to modus tollens.
(Contributed by NM, 26-Nov-1995.)
|
⊢ (𝜑 → ¬ 𝜓)
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) |
|
Theorem | mtbird 598 |
A deduction from a biconditional, similar to modus tollens.
(Contributed by NM, 10-May-1994.)
|
⊢ (𝜑 → ¬ 𝜒)
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | mtbii 599 |
An inference from a biconditional, similar to modus tollens.
(Contributed by NM, 27-Nov-1995.)
|
⊢ ¬ 𝜓
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) |
|
Theorem | mtbiri 600 |
An inference from a biconditional, similar to modus tollens.
(Contributed by NM, 24-Aug-1995.)
|
⊢ ¬ 𝜒
& ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |