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