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