![]() |
Metamath
Proof Explorer Theorem List (p. 8 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 | mpanl2 701 | An inference based on modus ponens. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ 𝜓 & ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | mpanl12 702 | An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.) |
⊢ 𝜑 & ⊢ 𝜓 & ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | mpanr1 703 | An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ 𝜓 & ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | mpanr2 704 | 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 705 | An inference based on modus ponens. (Contributed by NM, 24-Jul-2009.) |
⊢ 𝜓 & ⊢ 𝜒 & ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | mpanlr1 706 | An inference based on modus ponens. (Contributed by NM, 30-Dec-2004.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
⊢ 𝜓 & ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | mpbirand 707 | Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | mpbiran2d 708 | Detach truth from conjunction in biconditional. Deduction form. (Contributed by Peter Mazsa, 24-Sep-2022.) |
⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | mpbiran 709 | Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) |
⊢ 𝜓 & ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜒) | ||
Theorem | mpbiran2 710 | Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) |
⊢ 𝜒 & ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜓) | ||
Theorem | mpbir2an 711 | Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) |
⊢ 𝜓 & ⊢ 𝜒 & ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ 𝜑 | ||
Theorem | mpbi2and 712 | Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | mpbir2and 713 | Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) & ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | adantll 714 | Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜃 ∧ 𝜑) ∧ 𝜓) → 𝜒) | ||
Theorem | adantlr 715 | Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒) | ||
Theorem | adantrl 716 | Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒) | ||
Theorem | adantrr 717 | Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒) | ||
Theorem | adantlll 718 | Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 2-Dec-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | adantllr 719 | Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | adantlrl 720 | Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ (𝜏 ∧ 𝜓)) ∧ 𝜒) → 𝜃) | ||
Theorem | adantlrr 721 | Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜏)) ∧ 𝜒) → 𝜃) | ||
Theorem | adantrll 722 | Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ ((𝜏 ∧ 𝜓) ∧ 𝜒)) → 𝜃) | ||
Theorem | adantrlr 723 | Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜏) ∧ 𝜒)) → 𝜃) | ||
Theorem | adantrrl 724 | Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜏 ∧ 𝜒))) → 𝜃) | ||
Theorem | adantrrr 725 | Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜏))) → 𝜃) | ||
Theorem | ad2antrr 726 | Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜓) | ||
Theorem | ad2antlr 727 | Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (((𝜒 ∧ 𝜑) ∧ 𝜃) → 𝜓) | ||
Theorem | ad2antrl 728 | Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓) | ||
Theorem | ad2antll 729 | Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓) | ||
Theorem | ad3antrrr 730 | Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | ad3antlr 731 | Deduction adding three conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | ad4antr 732 | Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓) | ||
Theorem | ad4antlr 733 | Deduction adding 4 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓) | ||
Theorem | ad5antr 734 | Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) | ||
Theorem | ad5antlr 735 | Deduction adding 5 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) | ||
Theorem | ad6antr 736 | Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓) | ||
Theorem | ad6antlr 737 | Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓) | ||
Theorem | ad7antr 738 | Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓) | ||
Theorem | ad7antlr 739 | Deduction adding 7 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓) | ||
Theorem | ad8antr 740 | Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓) | ||
Theorem | ad8antlr 741 | Deduction adding 8 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓) | ||
Theorem | ad9antr 742 | Deduction adding 9 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜓) | ||
Theorem | ad9antlr 743 | Deduction adding 9 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜓) | ||
Theorem | ad10antr 744 | Deduction adding 10 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (((((((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜓) | ||
Theorem | ad10antlr 745 | Deduction adding 10 conjuncts to antecedent. (Contributed by Mario Carneiro, 5-Jan-2017.) (Proof shortened by Wolf Lammen, 5-Apr-2022.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (((((((((((𝜒 ∧ 𝜑) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜓) | ||
Theorem | ad2ant2l 746 | Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒) | ||
Theorem | ad2ant2r 747 | Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒) | ||
Theorem | ad2ant2lr 748 | Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒) | ||
Theorem | ad2ant2rl 749 | Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜏 ∧ 𝜓)) → 𝜒) | ||
Theorem | adantl3r 750 | Deduction adding 1 conjunct to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((((𝜑 ∧ 𝜂) ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | ad4ant13 751 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒) | ||
Theorem | ad4ant14 752 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒) | ||
Theorem | ad4ant23 753 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒) | ||
Theorem | ad4ant24 754 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) → 𝜒) | ||
Theorem | adantl4r 755 | Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ (((((𝜑 ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅) ⇒ ⊢ ((((((𝜑 ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅) | ||
Theorem | ad5ant12 756 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
Theorem | ad5ant13 757 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
Theorem | ad5ant14 758 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒) | ||
Theorem | ad5ant15 759 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒) | ||
Theorem | ad5ant23 760 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
Theorem | ad5ant24 761 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) ∧ 𝜂) → 𝜒) | ||
Theorem | ad5ant25 762 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒) | ||
Theorem | adantl5r 763 | Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ ((((((𝜑 ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅) ⇒ ⊢ (((((((𝜑 ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅) | ||
Theorem | adantl6r 764 | Deduction adding 1 conjunct to antecedent. (Contributed by Thierry Arnoux, 11-Feb-2018.) |
⊢ (((((((𝜑 ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅) ⇒ ⊢ ((((((((𝜑 ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜅) | ||
Theorem | pm3.33 765 | Theorem *3.33 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜒)) → (𝜑 → 𝜒)) | ||
Theorem | pm3.34 766 | Theorem *3.34 (Syll) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜓 → 𝜒) ∧ (𝜑 → 𝜓)) → (𝜑 → 𝜒)) | ||
Theorem | simpll 767 | Simplification of a conjunction. (Contributed by NM, 18-Mar-2007.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜑) | ||
Theorem | simplld 768 | Deduction form of simpll 767, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | simplr 769 | Simplification of a conjunction. (Contributed by NM, 20-Mar-2007.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜓) | ||
Theorem | simplrd 770 | Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | simprl 771 | Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜓) | ||
Theorem | simprld 772 | Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃))) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | simprr 773 | Simplification of a conjunction. (Contributed by NM, 21-Mar-2007.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜒) | ||
Theorem | simprrd 774 | Deduction form of simprr 773, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃))) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | simplll 775 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) (Proof shortened by Wolf Lammen, 6-Apr-2022.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑) | ||
Theorem | simpllr 776 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) (Proof shortened by Wolf Lammen, 6-Apr-2022.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜓) | ||
Theorem | simplrl 777 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓) | ||
Theorem | simplrr 778 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜒) | ||
Theorem | simprll 779 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) | ||
Theorem | simprlr 780 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) | ||
Theorem | simprrl 781 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜒) | ||
Theorem | simprrr 782 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃) | ||
Theorem | simp-4l 783 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
Theorem | simp-4r 784 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simp-5l 785 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑) | ||
Theorem | simp-5r 786 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓) | ||
Theorem | simp-6l 787 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑) | ||
Theorem | simp-6r 788 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) | ||
Theorem | simp-7l 789 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜑) | ||
Theorem | simp-7r 790 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓) | ||
Theorem | simp-8l 791 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜑) | ||
Theorem | simp-8r 792 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓) | ||
Theorem | simp-9l 793 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ ((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜑) | ||
Theorem | simp-9r 794 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ ((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓) | ||
Theorem | simp-10l 795 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ (((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜑) | ||
Theorem | simp-10r 796 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ (((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜓) | ||
Theorem | simp-11l 797 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ ((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜑) | ||
Theorem | simp-11r 798 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) (Proof shortened by Wolf Lammen, 24-May-2022.) |
⊢ ((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜓) | ||
Theorem | pm2.01da 799 | Deduction based on reductio ad absurdum. See pm2.01 188. (Contributed by Mario Carneiro, 9-Feb-2017.) |
⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | pm2.18da 800 | Deduction based on reductio ad absurdum. See pm2.18 128. (Contributed by Mario Carneiro, 9-Feb-2017.) |
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |