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