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