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