Home | Metamath
Proof Explorer Theorem List (p. 9 of 424) | < 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: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | simprrr 801 | Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) |
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃) | ||
Theorem | simp-4l 802 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
Theorem | simp-4r 803 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simp-5l 804 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜑) | ||
Theorem | simp-5r 805 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ ((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) → 𝜓) | ||
Theorem | simp-6l 806 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜑) | ||
Theorem | simp-6r 807 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) | ||
Theorem | simp-7l 808 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜑) | ||
Theorem | simp-7r 809 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ ((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓) | ||
Theorem | simp-8l 810 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜑) | ||
Theorem | simp-8r 811 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) → 𝜓) | ||
Theorem | simp-9l 812 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ ((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜑) | ||
Theorem | simp-9r 813 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ ((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) → 𝜓) | ||
Theorem | simp-10l 814 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜑) | ||
Theorem | simp-10r 815 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ (((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) → 𝜓) | ||
Theorem | simp-11l 816 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ ((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜑) | ||
Theorem | simp-11r 817 | Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.) |
⊢ ((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) → 𝜓) | ||
Theorem | jaob 818 | Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 9-Dec-2012.) |
⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓))) | ||
Theorem | adant423OLD 819 | Obsolete as of 2-Oct-2021. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜓) → 𝜒) | ||
Theorem | jaoian 820 | Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜃 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒) | ||
Theorem | jao1i 821 | Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.) |
⊢ (𝜓 → (𝜒 → 𝜑)) ⇒ ⊢ ((𝜑 ∨ 𝜓) → (𝜒 → 𝜑)) | ||
Theorem | jaodan 822 | Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜒) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒) | ||
Theorem | mpjaodan 823 | Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 26652. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜒) & ⊢ (𝜑 → (𝜓 ∨ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm4.77 824 | Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) ↔ ((𝜓 ∨ 𝜒) → 𝜑)) | ||
Theorem | pm2.63 825 | Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜑 ∨ 𝜓) → 𝜓)) | ||
Theorem | pm2.64 826 | Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ ¬ 𝜓) → 𝜑)) | ||
Theorem | pm2.61ian 827 | Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((¬ 𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜓 → 𝜒) | ||
Theorem | pm2.61dan 828 | Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | pm2.61ddan 829 | Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜃) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) & ⊢ ((𝜑 ∧ (¬ 𝜓 ∧ ¬ 𝜒)) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | pm2.61dda 830 | Elimination of two antecedents. (Contributed by NM, 9-Jul-2013.) |
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜃) & ⊢ ((𝜑 ∧ ¬ 𝜒) → 𝜃) & ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | condan 831 | Proof by contradiction. (Contributed by NM, 9-Feb-2006.) (Proof shortened by Wolf Lammen, 19-Jun-2014.) |
⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ ¬ 𝜓) → ¬ 𝜒) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | abai 832 | 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 | pm5.53 833 | Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ ((((𝜑 ∨ 𝜓) ∨ 𝜒) → 𝜃) ↔ (((𝜑 → 𝜃) ∧ (𝜓 → 𝜃)) ∧ (𝜒 → 𝜃))) | ||
Theorem | an12 834 | 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 835 | A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) | ||
Theorem | an13 836 | A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ (𝜒 ∧ (𝜓 ∧ 𝜑))) | ||
Theorem | an31 837 | A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜒 ∧ 𝜓) ∧ 𝜑)) | ||
Theorem | bianass 838 | An inference to merge two lists of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ ((𝜂 ∧ 𝜑) ↔ ((𝜂 ∧ 𝜓) ∧ 𝜒)) | ||
Theorem | an12s 839 | Swap two conjuncts in antecedent. The label suffix "s" means that an12 834 is combined with syl 17 (or a variant). (Contributed by NM, 13-Mar-1996.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜓 ∧ (𝜑 ∧ 𝜒)) → 𝜃) | ||
Theorem | ancom2s 840 | Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃) | ||
Theorem | an13s 841 | Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑)) → 𝜃) | ||
Theorem | an32s 842 | Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) | ||
Theorem | ancom1s 843 | Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜑) ∧ 𝜒) → 𝜃) | ||
Theorem | an31s 844 | Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜒 ∧ 𝜓) ∧ 𝜑) → 𝜃) | ||
Theorem | anass1rs 845 | Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜓) → 𝜃) | ||
Theorem | anabs1 846 | Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Wolf Lammen, 16-Nov-2013.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) ↔ (𝜑 ∧ 𝜓)) | ||
Theorem | anabs5 847 | Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 9-Dec-2012.) |
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓)) | ||
Theorem | anabs7 848 | Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 17-Nov-2013.) |
⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) ↔ (𝜑 ∧ 𝜓)) | ||
Theorem | a2and 849 | Deduction distributing a conjunction as embedded antecedent. (Contributed by AV, 25-Oct-2019.) (Proof shortened by Wolf Lammen, 19-Jan-2020.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜌) → (𝜏 → 𝜃))) & ⊢ (𝜑 → ((𝜓 ∧ 𝜌) → 𝜒)) ⇒ ⊢ (𝜑 → (((𝜓 ∧ 𝜒) → 𝜏) → ((𝜓 ∧ 𝜌) → 𝜃))) | ||
Theorem | anabsan 850 | Absorption of antecedent with conjunction. (Contributed by NM, 24-Mar-1996.) |
⊢ (((𝜑 ∧ 𝜑) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabss1 851 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabss4 852 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) |
⊢ (((𝜓 ∧ 𝜑) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabss5 853 | Absorption of antecedent into conjunction. (Contributed by NM, 10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.) |
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabsi5 854 | Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.) |
⊢ (𝜑 → ((𝜑 ∧ 𝜓) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabsi6 855 | Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜑) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabsi7 856 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.) |
⊢ (𝜓 → ((𝜑 ∧ 𝜓) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabsi8 857 | Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.) |
⊢ (𝜓 → ((𝜓 ∧ 𝜑) → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabss7 858 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 19-Nov-2013.) |
⊢ ((𝜓 ∧ (𝜑 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabsan2 859 | Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | anabss3 860 | Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | an4 861 | Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃))) | ||
Theorem | an42 862 | Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓))) | ||
Theorem | an43 863 | Rearrangement of 4 conjuncts. (Contributed by Rodolfo Medina, 24-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜒))) | ||
Theorem | an3 864 | A rearrangement of conjuncts. (Contributed by Rodolfo Medina, 25-Sep-2010.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → (𝜑 ∧ 𝜃)) | ||
Theorem | an4s 865 | Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) → 𝜏) | ||
Theorem | an42s 866 | Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜓)) → 𝜏) | ||
Theorem | anandi 867 | Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) | ||
Theorem | anandir 868 | Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒))) | ||
Theorem | anandis 869 | Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜏) | ||
Theorem | anandirs 870 | Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.) |
⊢ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜒)) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜏) | ||
Theorem | syl2an2 871 | syl2an 493 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜒 ∧ 𝜑) → 𝜃) & ⊢ ((𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜒 ∧ 𝜑) → 𝜏) | ||
Theorem | syl2an2r 872 | syl2anr 494 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) & ⊢ ((𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜏) | ||
Theorem | impbida 873 | Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜒) → 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | pm3.48 874 | Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))) | ||
Theorem | pm3.45 875 | Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) → ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))) | ||
Theorem | im2anan9 876 | Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂))) | ||
Theorem | im2anan9r 877 | Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ((𝜃 ∧ 𝜑) → ((𝜓 ∧ 𝜏) → (𝜒 ∧ 𝜂))) | ||
Theorem | anim12dan 878 | Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → (𝜒 ∧ 𝜏)) | ||
Theorem | orim12d 879 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏))) | ||
Theorem | orim1d 880 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃))) | ||
Theorem | orim2d 881 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒))) | ||
Theorem | orim2 882 | Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.38 883 | Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜒 ∨ 𝜑))) | ||
Theorem | pm2.36 884 | Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜒 ∨ 𝜑))) | ||
Theorem | pm2.37 885 | Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.73 886 | Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) → (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜓 ∨ 𝜒))) | ||
Theorem | pm2.74 887 | Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ ((𝜓 → 𝜑) → (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ 𝜒))) | ||
Theorem | orimdi 888 | Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013.) |
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) ↔ ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.76 889 | Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.75 890 | Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.) |
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.8 891 | Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜒))) | ||
Theorem | pm2.81 892 | Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜓 → (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜓) → ((𝜑 ∨ 𝜒) → (𝜑 ∨ 𝜃)))) | ||
Theorem | pm2.82 893 | Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) → (((𝜑 ∨ ¬ 𝜒) ∨ 𝜃) → ((𝜑 ∨ 𝜓) ∨ 𝜃))) | ||
Theorem | pm2.85 894 | Theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)) → (𝜑 ∨ (𝜓 → 𝜒))) | ||
Theorem | pm3.2ni 895 | Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.) |
⊢ ¬ 𝜑 & ⊢ ¬ 𝜓 ⇒ ⊢ ¬ (𝜑 ∨ 𝜓) | ||
Theorem | orabs 896 | Absorption of redundant internal disjunct. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 28-Feb-2014.) |
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ 𝜑)) | ||
Theorem | oranabs 897 | Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.) |
⊢ (((𝜑 ∨ ¬ 𝜓) ∧ 𝜓) ↔ (𝜑 ∧ 𝜓)) | ||
Theorem | pm5.1 898 | Two propositions are equivalent if they are both true. Theorem *5.1 of [WhiteheadRussell] p. 123. (Contributed by NM, 21-May-1994.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜑 ↔ 𝜓)) | ||
Theorem | pm5.21 899 | Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124. (Contributed by NM, 21-May-1994.) |
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → (𝜑 ↔ 𝜓)) | ||
Theorem | norbi 900 | If neither of two propositions is true, then these propositions are equivalent. (Contributed by BJ, 26-Apr-2019.) |
⊢ (¬ (𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |