Theorem List for Intuitionistic Logic Explorer - 501-600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | simplrl 501 |
Simplification of a conjunction. (Contributed by Jeff Hankins,
28-Jul-2009.)
|
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓) |
|
Theorem | simplrr 502 |
Simplification of a conjunction. (Contributed by Jeff Hankins,
28-Jul-2009.)
|
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒) |
|
Theorem | simprll 503 |
Simplification of a conjunction. (Contributed by Jeff Hankins,
28-Jul-2009.)
|
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) |
|
Theorem | simprlr 504 |
Simplification of a conjunction. (Contributed by Jeff Hankins,
28-Jul-2009.)
|
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
|
Theorem | simprrl 505 |
Simplification of a conjunction. (Contributed by Jeff Hankins,
28-Jul-2009.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒) |
|
Theorem | simprrr 506 |
Simplification of a conjunction. (Contributed by Jeff Hankins,
28-Jul-2009.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃) |
|
Theorem | simp-4l 507 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) |
|
Theorem | simp-4r 508 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
|
Theorem | simp-5l 509 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑) |
|
Theorem | simp-5r 510 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓) |
|
Theorem | simp-6l 511 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑) |
|
Theorem | simp-6r 512 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
|
Theorem | simp-7l 513 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜑) |
|
Theorem | simp-7r 514 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓) |
|
Theorem | simp-8l 515 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜑) |
|
Theorem | simp-8r 516 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓) |
|
Theorem | simp-9l 517 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ ((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜑) |
|
Theorem | simp-9r 518 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ ((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓) |
|
Theorem | simp-10l 519 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ (((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜑) |
|
Theorem | simp-10r 520 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ (((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜓) |
|
Theorem | simp-11l 521 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ ((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜑) |
|
Theorem | simp-11r 522 |
Simplification of a conjunction. (Contributed by Mario Carneiro,
4-Jan-2017.)
|
⊢ ((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜓) |
|
Theorem | pm4.87 523 |
Theorem *4.87 of [WhiteheadRussell] p.
122. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Eric Schmidt, 26-Oct-2006.)
|
⊢ (((((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) ∧ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒)))) ∧ ((𝜓 → (𝜑 → 𝜒)) ↔ ((𝜓 ∧ 𝜑) → 𝜒))) |
|
Theorem | abai 524 |
Introduce one conjunct as an antecedent to the other. "abai" stands
for
"and, biconditional, and, implication". (Contributed by NM,
12-Aug-1993.)
(Proof shortened by Wolf Lammen, 7-Dec-2012.)
|
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ (𝜑 → 𝜓))) |
|
Theorem | an12 525 |
Swap two conjuncts. Note that the first digit (1) in the label refers to
the outer conjunct position, and the next digit (2) to the inner conjunct
position. (Contributed by NM, 12-Mar-1995.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) |
|
Theorem | an32 526 |
A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof
shortened by Wolf Lammen, 25-Dec-2012.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
|
Theorem | an13 527 |
A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof
shortened by Wolf Lammen, 31-Dec-2012.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜑))) |
|
Theorem | an31 528 |
A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof
shortened by Wolf Lammen, 31-Dec-2012.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑)) |
|
Theorem | an12s 529 |
Swap two conjuncts in antecedent. The label suffix "s" means that
an12 525 is combined with syl 14 (or
a variant). (Contributed by NM,
13-Mar-1996.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃) |
|
Theorem | ancom2s 530 |
Inference commuting a nested conjunction in antecedent. (Contributed by
NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) |
|
Theorem | an13s 531 |
Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑)) → 𝜃) |
|
Theorem | an32s 532 |
Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) |
|
Theorem | ancom1s 533 |
Inference commuting a nested conjunction in antecedent. (Contributed by
NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃) |
|
Theorem | an31s 534 |
Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜒 ∧ 𝜓) ∧ 𝜑) → 𝜃) |
|
Theorem | anass1rs 535 |
Commutative-associative law for conjunction in an antecedent.
(Contributed by Jeff Madsen, 19-Jun-2011.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) |
|
Theorem | anabs1 536 |
Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.)
(Proof shortened by Wolf Lammen, 16-Nov-2013.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) ↔ (𝜑 ∧ 𝜓)) |
|
Theorem | anabs5 537 |
Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.)
(Proof shortened by Wolf Lammen, 9-Dec-2012.)
|
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓)) |
|
Theorem | anabs7 538 |
Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.)
(Proof shortened by Wolf Lammen, 17-Nov-2013.)
|
⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓)) |
|
Theorem | anabsan 539 |
Absorption of antecedent with conjunction. (Contributed by NM,
24-Mar-1996.) (Revised by NM, 18-Nov-2013.)
|
⊢ (((𝜑 ∧ 𝜑) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabss1 540 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabss4 541 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.)
|
⊢ (((𝜓 ∧ 𝜑) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabss5 542 |
Absorption of antecedent into conjunction. (Contributed by NM,
10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
|
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabsi5 543 |
Absorption of antecedent into conjunction. (Contributed by NM,
11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
|
⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabsi6 544 |
Absorption of antecedent into conjunction. (Contributed by NM,
14-Aug-2000.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜑) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabsi7 545 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
|
⊢ (𝜓 → ((𝜑 ∧ 𝜓) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabsi8 546 |
Absorption of antecedent into conjunction. (Contributed by NM,
26-Sep-1999.)
|
⊢ (𝜓 → ((𝜓 ∧ 𝜑) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabss7 547 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 19-Nov-2013.)
|
⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabsan2 548 |
Absorption of antecedent with conjunction. (Contributed by NM,
10-May-2004.) (Revised by NM, 1-Jan-2013.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | anabss3 549 |
Absorption of antecedent into conjunction. (Contributed by NM,
20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | an4 550 |
Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃))) |
|
Theorem | an42 551 |
Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓))) |
|
Theorem | an4s 552 |
Inference rearranging 4 conjuncts in antecedent. (Contributed by NM,
10-Aug-1995.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) |
|
Theorem | an42s 553 |
Inference rearranging 4 conjuncts in antecedent. (Contributed by NM,
10-Aug-1995.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏) |
|
Theorem | anandi 554 |
Distribution of conjunction over conjunction. (Contributed by NM,
14-Aug-1995.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) |
|
Theorem | anandir 555 |
Distribution of conjunction over conjunction. (Contributed by NM,
24-Aug-1995.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒))) |
|
Theorem | anandis 556 |
Inference that undistributes conjunction in the antecedent.
(Contributed by NM, 7-Jun-2004.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏) |
|
Theorem | anandirs 557 |
Inference that undistributes conjunction in the antecedent.
(Contributed by NM, 7-Jun-2004.)
|
⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜏) |
|
Theorem | syl2an2 558 |
syl2an 283 with antecedents in standard conjunction form.
(Contributed by
Alan Sare, 27-Aug-2016.)
|
⊢ (𝜑 → 𝜓)
& ⊢ ((𝜒 ∧ 𝜑) → 𝜃)
& ⊢ ((𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜒 ∧ 𝜑) → 𝜏) |
|
Theorem | syl2an2r 559 |
syl2anr 284 with antecedents in standard conjunction form.
(Contributed
by Alan Sare, 27-Aug-2016.)
|
⊢ (𝜑 → 𝜓)
& ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
& ⊢ ((𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜏) |
|
Theorem | impbida 560 |
Deduce an equivalence from two implications. (Contributed by NM,
17-Feb-2007.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒)
& ⊢ ((𝜑 ∧ 𝜒) → 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
|
Theorem | pm3.45 561 |
Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed
by NM,
3-Jan-2005.)
|
⊢ ((𝜑 → 𝜓) → ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))) |
|
Theorem | im2anan9 562 |
Deduction joining nested implications to form implication of
conjunctions. (Contributed by NM, 29-Feb-1996.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂))) |
|
Theorem | im2anan9r 563 |
Deduction joining nested implications to form implication of
conjunctions. (Contributed by NM, 29-Feb-1996.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂))) |
|
Theorem | anim12dan 564 |
Conjoin antecedents and consequents in a deduction. (Contributed by
Mario Carneiro, 12-May-2014.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒)
& ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏)) |
|
Theorem | pm5.1 565 |
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 566 |
Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed
by NM,
3-Jan-2005.) (Revised by NM, 27-Nov-2013.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∧ 𝜒))) |
|
Theorem | jcab 567 |
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 568 |
Theorem *4.76 of [WhiteheadRussell] p.
121. (Contributed by NM,
3-Jan-2005.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒))) |
|
Theorem | pm4.38 569 |
Theorem *4.38 of [WhiteheadRussell] p.
118. (Contributed by NM,
3-Jan-2005.)
|
⊢ (((𝜑 ↔ 𝜒) ∧ (𝜓 ↔ 𝜃)) → ((𝜑 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃))) |
|
Theorem | bi2anan9 570 |
Deduction joining two equivalences to form equivalence of conjunctions.
(Contributed by NM, 31-Jul-1995.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜏 ↔ 𝜂)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
|
Theorem | bi2anan9r 571 |
Deduction joining two equivalences to form equivalence of conjunctions.
(Contributed by NM, 19-Feb-1996.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜏 ↔ 𝜂)) ⇒ ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) |
|
Theorem | bi2bian9 572 |
Deduction joining two biconditionals with different antecedents.
(Contributed by NM, 12-May-2004.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜏 ↔ 𝜂)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ↔ 𝜏) ↔ (𝜒 ↔ 𝜂))) |
|
Theorem | pm5.33 573 |
Theorem *5.33 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
⊢ ((𝜑 ∧ (𝜓 → 𝜒)) ↔ (𝜑 ∧ ((𝜑 ∧ 𝜓) → 𝜒))) |
|
Theorem | pm5.36 574 |
Theorem *5.36 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
⊢ ((𝜑 ∧ (𝜑 ↔ 𝜓)) ↔ (𝜓 ∧ (𝜑 ↔ 𝜓))) |
|
Theorem | bianabs 575 |
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 576 |
'Not' introduction. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.)
|
⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑) |
|
Axiom | ax-in2 577 |
'Not' elimination. One of the axioms of propositional logic.
(Contributed by Mario Carneiro, 31-Jan-2015.)
|
⊢ (¬ 𝜑 → (𝜑 → 𝜓)) |
|
Theorem | pm2.01 578 |
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 783 which only holds for some propositions.
(Contributed by
Mario Carneiro, 12-May-2015.)
|
⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑) |
|
Theorem | pm2.21 579 |
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 580 |
Deduction based on reductio ad absurdum. (Contributed by NM,
18-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ (𝜑 → (𝜓 → ¬ 𝜓)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | pm2.21d 581 |
A contradiction implies anything. Deduction from pm2.21 579.
(Contributed by NM, 10-Feb-1996.)
|
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) |
|
Theorem | pm2.21dd 582 |
A contradiction implies anything. Deduction from pm2.21 579.
(Contributed by Mario Carneiro, 9-Feb-2017.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | pm2.24 583 |
Theorem *2.24 of [WhiteheadRussell] p.
104. (Contributed by NM,
3-Jan-2005.)
|
⊢ (𝜑 → (¬ 𝜑 → 𝜓)) |
|
Theorem | pm2.24d 584 |
Deduction version of pm2.24 583. (Contributed by NM, 30-Jan-2006.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
|
Theorem | pm2.24i 585 |
Inference version of pm2.24 583. (Contributed by NM, 20-Aug-2001.)
(Revised by Mario Carneiro, 31-Jan-2015.)
|
⊢ 𝜑 ⇒ ⊢ (¬ 𝜑 → 𝜓) |
|
Theorem | con2d 586 |
A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised
by NM, 12-Feb-2013.)
|
⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 → ¬ 𝜓)) |
|
Theorem | mt2d 587 |
Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
|
⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | nsyl3 588 |
A negated syllogism inference. (Contributed by NM, 1-Dec-1995.)
(Revised by NM, 13-Jun-2013.)
|
⊢ (𝜑 → ¬ 𝜓)
& ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜒 → ¬ 𝜑) |
|
Theorem | con2i 589 |
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 590 |
A negated syllogism inference. (Contributed by NM, 31-Dec-1993.)
(Proof shortened by Wolf Lammen, 2-Mar-2013.)
|
⊢ (𝜑 → ¬ 𝜓)
& ⊢ (𝜒 → 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜒) |
|
Theorem | notnot 591 |
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 784). (Contributed by NM,
28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
|
⊢ (𝜑 → ¬ ¬ 𝜑) |
|
Theorem | notnotd 592 |
Deduction associated with notnot 591 and notnoti 606. (Contributed by
Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf
Lammen, 27-Mar-2021.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ¬ ¬ 𝜓) |
|
Theorem | con3d 593 |
A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised
by NM, 31-Jan-2015.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓)) |
|
Theorem | con3i 594 |
A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by Wolf Lammen, 20-Jun-2013.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (¬ 𝜓 → ¬ 𝜑) |
|
Theorem | con3rr3 595 |
Rotate through consequent right. (Contributed by Wolf Lammen,
3-Nov-2013.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (¬ 𝜒 → (𝜑 → ¬ 𝜓)) |
|
Theorem | con3dimp 596 |
Variant of con3d 593 with importation. (Contributed by Jonathan
Ben-Naim,
3-Jun-2011.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓) |
|
Theorem | pm2.01da 597 |
Deduction based on reductio ad absurdum. (Contributed by Mario
Carneiro, 9-Feb-2017.)
|
⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜓) |
|
Theorem | pm3.2im 598 |
In classical logic, this is just a restatement of pm3.2 137. In
intuitionistic logic, it still holds, but is weaker than pm3.2.
(Contributed by Mario Carneiro, 12-May-2015.)
|
⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓))) |
|
Theorem | expi 599 |
An exportation inference. (Contributed by NM, 5-Aug-1993.) (Proof
shortened by O'Cat, 28-Nov-2008.)
|
⊢ (¬ (𝜑 → ¬ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) |
|
Theorem | pm2.65i 600 |
Inference rule for proof by contradiction. (Contributed by NM,
18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ ¬ 𝜑 |