![]() |
Metamath
Proof Explorer Theorem List (p. 7 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sylancbr 601 | A syllogism inference combined with contraction. (Contributed by NM, 3-Sep-2004.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜒 ↔ 𝜑) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | syldanl 602 | A syllogism deduction with conjoined antecedents. (Contributed by Jeff Madsen, 20-Jun-2011.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏) | ||
Theorem | syland 603 | A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏)) | ||
Theorem | sylani 604 | A syllogism inference. (Contributed by NM, 2-May-1996.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜓 → ((𝜑 ∧ 𝜃) → 𝜏)) | ||
Theorem | sylan2d 605 | A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜏)) ⇒ ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜏)) | ||
Theorem | sylan2i 606 | A syllogism inference. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝜑 → 𝜃) & ⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜓 → ((𝜒 ∧ 𝜑) → 𝜏)) | ||
Theorem | syl2ani 607 | A syllogism inference. (Contributed by NM, 3-Aug-1999.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜂 → 𝜃) & ⊢ (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜓 → ((𝜑 ∧ 𝜂) → 𝜏)) | ||
Theorem | syl2and 608 | A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂)) | ||
Theorem | anim12d 609 | Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) | ||
Theorem | anim12d1 610 | Variant of anim12d 609 where the second implication does not depend on the antecedent. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) | ||
Theorem | anim1d 611 | Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃))) | ||
Theorem | anim2d 612 | Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒))) | ||
Theorem | anim12i 613 | Conjoin antecedents and consequents of two premises. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃)) | ||
Theorem | anim12ci 614 | Variant of anim12i 613 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜃 ∧ 𝜓)) | ||
Theorem | anim1i 615 | Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | ||
Theorem | anim1ci 616 | Introduce conjunct to both sides of an implication. (Contributed by Peter Mazsa, 24-Sep-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜒 ∧ 𝜓)) | ||
Theorem | anim2i 617 | Introduce conjunct to both sides of an implication. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓)) | ||
Theorem | anim12ii 618 | Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007.) (Proof shortened by Wolf Lammen, 19-Jul-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜓 → 𝜏)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → (𝜒 ∧ 𝜏))) | ||
Theorem | anim12dan 619 | Conjoin antecedents and consequents in a deduction. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏)) | ||
Theorem | im2anan9 620 | Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂))) | ||
Theorem | im2anan9r 621 | Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂))) | ||
Theorem | pm3.45 622 | Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) → ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))) | ||
Theorem | anbi2i 623 | Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓)) | ||
Theorem | anbi1i 624 | Introduce a right conjunct to both sides of a logical equivalence. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒)) | ||
Theorem | anbi2ci 625 | Variant of anbi2i 623 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓)) | ||
Theorem | anbi1ci 626 | Variant of anbi1i 624 with commutation. (Contributed by Peter Mazsa, 7-Mar-2020.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑) ↔ (𝜓 ∧ 𝜒)) | ||
Theorem | bianbi 627 | Exchanging conjunction in a biconditional. (Contributed by Peter Mazsa, 31-Jul-2023.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) & ⊢ (𝜓 ↔ 𝜃) ⇒ ⊢ (𝜑 ↔ (𝜃 ∧ 𝜒)) | ||
Theorem | anbi12i 628 | Conjoin both sides of two equivalences. (Contributed by NM, 12-Mar-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃)) | ||
Theorem | anbi12ci 629 | Variant of anbi12i 628 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) ↔ (𝜃 ∧ 𝜓)) | ||
Theorem | anbi2d 630 | Deduction adding a left conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜃 ∧ 𝜒))) | ||
Theorem | anbi1d 631 | Deduction adding a right conjunct to both sides of a logical equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 16-Nov-2013.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜃))) | ||
Theorem | anbi12d 632 | Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏))) | ||
Theorem | anbi1 633 | Introduce a right conjunct to both sides of a logical equivalence. Theorem *4.36 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | anbi2 634 | Introduce a left conjunct to both sides of a logical equivalence. (Contributed by NM, 16-Nov-2013.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∧ 𝜑) ↔ (𝜒 ∧ 𝜓))) | ||
Theorem | anbi1cd 635 | Introduce a proposition as left conjunct on the left-hand side and right conjunct on the right-hand side of an equivalence. Deduction form. (Contributed by Peter Mazsa, 22-May-2021.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃))) | ||
Theorem | an2anr 636 | Double commutation in conjunction. (Contributed by Peter Mazsa, 27-Jun-2019.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜓 ∧ 𝜑) ∧ (𝜃 ∧ 𝜒))) | ||
Theorem | pm4.38 637 | Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ↔ 𝜒) ∧ (𝜓 ↔ 𝜃)) → ((𝜑 ∧ 𝜓) ↔ (𝜒 ∧ 𝜃))) | ||
Theorem | bi2anan9 638 | Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜏 ↔ 𝜂)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) | ||
Theorem | bi2anan9r 639 | Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜏 ↔ 𝜂)) ⇒ ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) ↔ (𝜒 ∧ 𝜂))) | ||
Theorem | bi2bian9 640 | Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜏 ↔ 𝜂)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ↔ 𝜏) ↔ (𝜒 ↔ 𝜂))) | ||
Theorem | anbiim 641 | Adding biconditional when antecedents are conjuncted. (Contributed by metakunt, 16-Apr-2024.) (Proof shortened by Wolf Lammen, 7-May-2025.) |
⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜓 → (𝜃 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) | ||
Theorem | bianass 642 | An inference to merge two lists of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ ((𝜂 ∧ 𝜑) ↔ ((𝜂 ∧ 𝜓) ∧ 𝜒)) | ||
Theorem | bianassc 643 | An inference to merge two lists of conjuncts. (Contributed by Peter Mazsa, 24-Sep-2022.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ ((𝜂 ∧ 𝜑) ↔ ((𝜓 ∧ 𝜂) ∧ 𝜒)) | ||
Theorem | an21 644 | Swap two conjuncts. (Contributed by Peter Mazsa, 18-Sep-2022.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | ||
Theorem | an12 645 | 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.) (Proof shortened by Peter Mazsa, 18-Sep-2022.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜓 ∧ (𝜑 ∧ 𝜒))) | ||
Theorem | an32 646 | A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) | ||
Theorem | an13 647 | A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜑))) | ||
Theorem | an31 648 | A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑)) | ||
Theorem | an12s 649 | Swap two conjuncts in antecedent. The label suffix "s" means that an12 645 is combined with syl 17 (or a variant). (Contributed by NM, 13-Mar-1996.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃) | ||
Theorem | ancom2s 650 | Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) | ||
Theorem | an13s 651 | Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑)) → 𝜃) | ||
Theorem | an32s 652 | Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) | ||
Theorem | ancom1s 653 | Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃) | ||
Theorem | an31s 654 | Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜒 ∧ 𝜓) ∧ 𝜑) → 𝜃) | ||
Theorem | anass1rs 655 | Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) | ||
Theorem | an4 656 | Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃))) | ||
Theorem | an42 657 | Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓))) | ||
Theorem | an43 658 | Rearrangement of 4 conjuncts. (Contributed by Rodolfo Medina, 24-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜒))) | ||
Theorem | an3 659 | A rearrangement of conjuncts. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → (𝜑 ∧ 𝜃)) | ||
Theorem | an4s 660 | Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) | ||
Theorem | an42s 661 | Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏) | ||
Theorem | anabs1 662 | Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Wolf Lammen, 16-Nov-2013.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) ↔ (𝜑 ∧ 𝜓)) | ||
Theorem | anabs5 663 | Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 9-Dec-2012.) |
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓)) | ||
Theorem | anabs7 664 | Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 17-Nov-2013.) |
⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓)) | ||
Theorem | anabsan 665 | Absorption of antecedent with conjunction. (Contributed by NM, 24-Mar-1996.) |
⊢ (((𝜑 ∧ 𝜑) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabss1 666 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabss4 667 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) |
⊢ (((𝜓 ∧ 𝜑) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabss5 668 | Absorption of antecedent into conjunction. (Contributed by NM, 10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.) |
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabsi5 669 | Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.) |
⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabsi6 670 | Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜑) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabsi7 671 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.) |
⊢ (𝜓 → ((𝜑 ∧ 𝜓) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabsi8 672 | Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.) |
⊢ (𝜓 → ((𝜓 ∧ 𝜑) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabss7 673 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 19-Nov-2013.) |
⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabsan2 674 | Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabss3 675 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anandi 676 | Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) | ||
Theorem | anandir 677 | Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒))) | ||
Theorem | anandis 678 | Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏) | ||
Theorem | anandirs 679 | Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.) |
⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜏) | ||
Theorem | sylanl1 680 | A syllogism inference. (Contributed by NM, 10-Mar-2005.) |
⊢ (𝜑 → 𝜓) & ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | sylanl2 681 | A syllogism inference. (Contributed by NM, 1-Jan-2005.) |
⊢ (𝜑 → 𝜒) & ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜃) → 𝜏) | ||
Theorem | sylanr1 682 | A syllogism inference. (Contributed by NM, 9-Apr-2005.) |
⊢ (𝜑 → 𝜒) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜃)) → 𝜏) | ||
Theorem | sylanr2 683 | A syllogism inference. (Contributed by NM, 9-Apr-2005.) |
⊢ (𝜑 → 𝜃) & ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜑)) → 𝜏) | ||
Theorem | syl6an 684 | A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ ((𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜒 → 𝜏)) | ||
Theorem | syl2an2r 685 | syl2anr 597 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Mar-2022.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) & ⊢ ((𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜏) | ||
Theorem | syl2an2 686 | syl2an 596 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜒 ∧ 𝜑) → 𝜃) & ⊢ ((𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜒 ∧ 𝜑) → 𝜏) | ||
Theorem | mpdan 687 | An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | mpancom 688 | An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
⊢ (𝜓 → 𝜑) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜓 → 𝜒) | ||
Theorem | mpidan 689 | A deduction which "stacks" a hypothesis. (Contributed by Stanislas Polu, 9-Mar-2020.) (Proof shortened by Wolf Lammen, 28-Mar-2021.) |
⊢ (𝜑 → 𝜒) & ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | ||
Theorem | mpan 690 | An inference based on modus ponens. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
⊢ 𝜑 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜓 → 𝜒) | ||
Theorem | mpan2 691 | An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |
⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | mp2an 692 | An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | mp4an 693 | An inference based on modus ponens. (Contributed by Jeff Madsen, 15-Jun-2010.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ 𝜃 & ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ 𝜏 | ||
Theorem | mpan2d 694 | A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | mpand 695 | A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → (𝜒 → 𝜃)) | ||
Theorem | mpani 696 | An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |
⊢ 𝜓 & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → (𝜒 → 𝜃)) | ||
Theorem | mpan2i 697 | An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.) |
⊢ 𝜒 & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | mp2ani 698 | An inference based on modus ponens. (Contributed by NM, 12-Dec-2004.) |
⊢ 𝜓 & ⊢ 𝜒 & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | mp2and 699 | A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | mpanl1 700 | An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
⊢ 𝜑 & ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜒) → 𝜃) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |