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