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