![]() |
Metamath
Proof Explorer Theorem List (p. 6 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | simplbi 501 | Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | simprbda 502 | Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.) |
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | simplbda 503 | Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007.) |
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | ||
Theorem | simplbi2 504 | Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜒 → 𝜑)) | ||
Theorem | simplbi2comt 505 | Closed form of simplbi2com 506. (Contributed by Alan Sare, 22-Jul-2012.) |
⊢ ((𝜑 ↔ (𝜓 ∧ 𝜒)) → (𝜒 → (𝜓 → 𝜑))) | ||
Theorem | simplbi2com 506 | A deduction eliminating a conjunct, similar to simplbi2 504. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Wolf Lammen, 10-Nov-2012.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜒 → (𝜓 → 𝜑)) | ||
Theorem | simpl2im 507 | Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.) (Proof shortened by Wolf Lammen, 26-Mar-2022.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒)) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | simplbiim 508 | Implication from an eliminated conjunct equivalent to the antecedent. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Wolf Lammen, 26-Mar-2022.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | impel 509 | An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜃) → 𝜒) | ||
Theorem | mpan9 510 | Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → (𝜓 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | sylan9 511 | Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜒 → 𝜏)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → 𝜏)) | ||
Theorem | sylan9r 512 | Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜒 → 𝜏)) ⇒ ⊢ ((𝜃 ∧ 𝜑) → (𝜓 → 𝜏)) | ||
Theorem | sylan9bb 513 | Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜒 ↔ 𝜏)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜏)) | ||
Theorem | sylan9bbr 514 | Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜒 ↔ 𝜏)) ⇒ ⊢ ((𝜃 ∧ 𝜑) → (𝜓 ↔ 𝜏)) | ||
Theorem | jca 515 | Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). Deduction form of pm3.2 473 and pm3.2i 474. Its associated deduction is jcad 516. Equivalent to the natural deduction rule ∧ I (∧ introduction), see natded 28188. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒)) | ||
Theorem | jcad 516 | Deduction conjoining the consequents of two implications. Deduction form of jca 515 and double deduction form of pm3.2 473 and pm3.2i 474. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) | ||
Theorem | jca2 517 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜓 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) | ||
Theorem | jca31 518 | Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) | ||
Theorem | jca32 519 | Join three consequents. (Contributed by FL, 1-Aug-2009.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃))) | ||
Theorem | jcai 520 | Deduction replacing implication with conjunction. (Contributed by NM, 15-Jul-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒)) | ||
Theorem | jcab 521 | Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 27-Nov-2013.) |
⊢ ((𝜑 → (𝜓 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (𝜑 → 𝜒))) | ||
Theorem | pm4.76 522 | Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒))) | ||
Theorem | jctil 523 | Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 ⇒ ⊢ (𝜑 → (𝜒 ∧ 𝜓)) | ||
Theorem | jctir 524 | Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒)) | ||
Theorem | jccir 525 | Inference conjoining a consequent of a consequent to the right of the consequent in an implication. See also ex-natded5.3i 28194. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by AV, 20-Aug-2019.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒)) | ||
Theorem | jccil 526 | Inference conjoining a consequent of a consequent to the left of the consequent in an implication. Remark: One can also prove this theorem using syl 17 and jca 515 (as done in jccir 525), which would be 4 bytes shorter, but one step longer than the current proof. (Proof modification is discouraged.) (Contributed by AV, 20-Aug-2019.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → (𝜒 ∧ 𝜓)) | ||
Theorem | jctl 527 | Inference conjoining a theorem to the left of a consequent. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.) |
⊢ 𝜓 ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜑)) | ||
Theorem | jctr 528 | Inference conjoining a theorem to the right of a consequent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.) |
⊢ 𝜓 ⇒ ⊢ (𝜑 → (𝜑 ∧ 𝜓)) | ||
Theorem | jctild 529 | Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒))) | ||
Theorem | jctird 530 | Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) | ||
Theorem | iba 531 | Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.) |
⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) | ||
Theorem | ibar 532 | Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.) |
⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | ||
Theorem | biantru 533 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 26-May-1993.) |
⊢ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑)) | ||
Theorem | biantrur 534 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.) |
⊢ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓)) | ||
Theorem | biantrud 535 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓))) | ||
Theorem | biantrurd 536 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | bianfi 537 | A wff conjoined with falsehood is false. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.) |
⊢ ¬ 𝜑 ⇒ ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑)) | ||
Theorem | bianfd 538 | A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | baib 539 | Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜑 ↔ 𝜒)) | ||
Theorem | baibr 540 | Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜒 ↔ 𝜑)) | ||
Theorem | rbaibr 541 | Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜒 → (𝜓 ↔ 𝜑)) | ||
Theorem | rbaib 542 | Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) (Proof shortened by Wolf Lammen, 19-Jan-2020.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜒 → (𝜑 ↔ 𝜓)) | ||
Theorem | baibd 543 | Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃)) | ||
Theorem | rbaibd 544 | Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.) |
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) | ||
Theorem | bianabs 545 | Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.) |
⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | ||
Theorem | pm5.44 546 | Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜒) ↔ (𝜑 → (𝜓 ∧ 𝜒)))) | ||
Theorem | pm5.42 547 | Theorem *5.42 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))) | ||
Theorem | ancl 548 | Conjoin antecedent to left of consequent. (Contributed by NM, 15-Aug-1994.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜑 ∧ 𝜓))) | ||
Theorem | anclb 549 | Conjoin antecedent to left of consequent. Theorem *4.7 of [WhiteheadRussell] p. 120. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜑 ∧ 𝜓))) | ||
Theorem | ancr 550 | Conjoin antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜓 ∧ 𝜑))) | ||
Theorem | ancrb 551 | Conjoin antecedent to right of consequent. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜓 ∧ 𝜑))) | ||
Theorem | ancli 552 | Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜑 ∧ 𝜓)) | ||
Theorem | ancri 553 | Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜑)) | ||
Theorem | ancld 554 | Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒))) | ||
Theorem | ancrd 555 | Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓))) | ||
Theorem | impac 556 | Importation with conjunction in consequent. (Contributed by NM, 9-Aug-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∧ 𝜓)) | ||
Theorem | anc2l 557 | Conjoin antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 14-Jul-2013.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))) | ||
Theorem | anc2r 558 | Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜒 ∧ 𝜑)))) | ||
Theorem | anc2li 559 | Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒))) | ||
Theorem | anc2ri 560 | Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜑))) | ||
Theorem | pm4.71 561 | Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 2-Dec-2012.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜑 ∧ 𝜓))) | ||
Theorem | pm4.71r 562 | Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 25-Jul-1999.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜓 ∧ 𝜑))) | ||
Theorem | pm4.71i 563 | Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓)) | ||
Theorem | pm4.71ri 564 | Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑)) | ||
Theorem | pm4.71d 565 | Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by Mario Carneiro, 25-Dec-2016.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | pm4.71rd 566 | Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜓))) | ||
Theorem | pm4.24 567 | Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) |
⊢ (𝜑 ↔ (𝜑 ∧ 𝜑)) | ||
Theorem | anidm 568 | Idempotent law for conjunction. (Contributed by NM, 8-Jan-2004.) (Proof shortened by Wolf Lammen, 14-Mar-2014.) |
⊢ ((𝜑 ∧ 𝜑) ↔ 𝜑) | ||
Theorem | anidmdbi 569 | Conjunction idempotence with antecedent. (Contributed by Roy F. Longton, 8-Aug-2005.) |
⊢ ((𝜑 → (𝜓 ∧ 𝜓)) ↔ (𝜑 → 𝜓)) | ||
Theorem | anidms 570 | Inference from idempotent law for conjunction. (Contributed by NM, 15-Jun-1994.) |
⊢ ((𝜑 ∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | imdistan 571 | Distribution of implication with conjunction. (Contributed by NM, 31-May-1999.) (Proof shortened by Wolf Lammen, 6-Dec-2012.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))) | ||
Theorem | imdistani 572 | Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒)) | ||
Theorem | imdistanri 573 | Distribution of implication with conjunction. (Contributed by NM, 8-Jan-2002.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ ((𝜓 ∧ 𝜑) → (𝜒 ∧ 𝜑)) | ||
Theorem | imdistand 574 | Distribution of implication with conjunction (deduction form). (Contributed by NM, 27-Aug-2004.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃))) | ||
Theorem | imdistanda 575 | Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜃))) | ||
Theorem | pm5.3 576 | Theorem *5.3 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))) | ||
Theorem | pm5.32 577 | Distribution of implication over biconditional. Theorem *5.32 of [WhiteheadRussell] p. 125. (Contributed by NM, 1-Aug-1994.) |
⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))) | ||
Theorem | pm5.32i 578 | Distribution of implication over biconditional (inference form). (Contributed by NM, 1-Aug-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)) | ||
Theorem | pm5.32ri 579 | Distribution of implication over biconditional (inference form). (Contributed by NM, 12-Mar-1995.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜓 ∧ 𝜑) ↔ (𝜒 ∧ 𝜑)) | ||
Theorem | pm5.32d 580 | Distribution of implication over biconditional (deduction form). (Contributed by NM, 29-Oct-1996.) |
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) | ||
Theorem | pm5.32rd 581 | Distribution of implication over biconditional (deduction form). (Contributed by NM, 25-Dec-2004.) |
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) ⇒ ⊢ (𝜑 → ((𝜒 ∧ 𝜓) ↔ (𝜃 ∧ 𝜓))) | ||
Theorem | pm5.32da 582 | Distribution of implication over biconditional (deduction form). (Contributed by NM, 9-Dec-2006.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜃))) | ||
Theorem | sylan 583 | A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | sylanb 584 | A syllogism inference. (Contributed by NM, 18-May-1994.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | sylanbr 585 | A syllogism inference. (Contributed by NM, 18-May-1994.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | sylanbrc 586 | Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | syl2anc 587 | Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | syl2anc2 588 | Double syllogism inference combined with contraction. (Contributed by BTernaryTau, 29-Sep-2023.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜓 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | sylancl 589 | Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | sylancr 590 | Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ 𝜓 & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | sylancom 591 | Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜒 ∧ 𝜓) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | ||
Theorem | sylanblc 592 | Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ ((𝜓 ∧ 𝜒) ↔ 𝜃) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | sylanblrc 593 | Syllogism inference combined with a biconditional. (Contributed by BJ, 25-Apr-2019.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 & ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | syldan 594 | A syllogism deduction with conjoined antecedents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜃) | ||
Theorem | sylan2 595 | A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.) |
⊢ (𝜑 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜃) | ||
Theorem | sylan2b 596 | A syllogism inference. (Contributed by NM, 21-Apr-1994.) |
⊢ (𝜑 ↔ 𝜒) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜃) | ||
Theorem | sylan2br 597 | A syllogism inference. (Contributed by NM, 21-Apr-1994.) |
⊢ (𝜒 ↔ 𝜑) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜃) | ||
Theorem | syl2an 598 | A double syllogism inference. For an implication-only version, see syl2im 40. (Contributed by NM, 31-Jan-1997.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜏 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜏) → 𝜃) | ||
Theorem | syl2anr 599 | A double syllogism inference. For an implication-only version, see syl2imc 41. (Contributed by NM, 17-Sep-2013.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜏 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜏 ∧ 𝜑) → 𝜃) | ||
Theorem | syl2anb 600 | A double syllogism inference. (Contributed by NM, 29-Jul-1999.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜏 ↔ 𝜒) & ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |