![]() |
Metamath
Proof Explorer Theorem List (p. 6 of 431) | < 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-28084) |
![]() (28085-29609) |
![]() (29610-43064) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | syl2and 501 | A syllogism deduction. (Contributed by NM, 15-Dec-2004.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂)) | ||
Theorem | biimpa 502 | Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | biimpar 503 | Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜓) | ||
Theorem | biimpac 504 | Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) | ||
Theorem | biimparc 505 | Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜒 ∧ 𝜑) → 𝜓) | ||
Theorem | animorl 506 | Conjunction implies disjunction with one common formula (1/4). (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∨ 𝜒)) | ||
Theorem | animorr 507 | Conjunction implies disjunction with one common formula (2/4). (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∨ 𝜓)) | ||
Theorem | animorlr 508 | Conjunction implies disjunction with one common formula (3/4). (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∨ 𝜑)) | ||
Theorem | animorrl 509 | Conjunction implies disjunction with one common formula (4/4). (Contributed by BJ, 4-Oct-2019.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒)) | ||
Theorem | ianor 510 | Negated conjunction in terms of disjunction (De Morgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓)) | ||
Theorem | anor 511 | Conjunction in terms of disjunction (De Morgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 3-Nov-2012.) |
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓)) | ||
Theorem | ioran 512 | Negated disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓)) | ||
Theorem | pm4.52 513 | Theorem *4.52 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.) |
⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (¬ 𝜑 ∨ 𝜓)) | ||
Theorem | pm4.53 514 | Theorem *4.53 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 ∧ ¬ 𝜓) ↔ (¬ 𝜑 ∨ 𝜓)) | ||
Theorem | pm4.54 515 | Theorem *4.54 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.) |
⊢ ((¬ 𝜑 ∧ 𝜓) ↔ ¬ (𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm4.55 516 | Theorem *4.55 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (¬ 𝜑 ∧ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm4.56 517 | Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓)) | ||
Theorem | oran 518 | Disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ ((𝜑 ∨ 𝜓) ↔ ¬ (¬ 𝜑 ∧ ¬ 𝜓)) | ||
Theorem | pm4.57 519 | Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (¬ 𝜑 ∧ ¬ 𝜓) ↔ (𝜑 ∨ 𝜓)) | ||
Theorem | pm3.1 520 | Theorem *3.1 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∧ 𝜓) → ¬ (¬ 𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm3.11 521 | Theorem *3.11 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (¬ 𝜑 ∨ ¬ 𝜓) → (𝜑 ∧ 𝜓)) | ||
Theorem | pm3.12 522 | Theorem *3.12 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓)) | ||
Theorem | pm3.13 523 | Theorem *3.13 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓)) | ||
Theorem | pm3.14 524 | Theorem *3.14 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓)) | ||
Theorem | iba 525 | Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.) |
⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) | ||
Theorem | ibar 526 | Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.) |
⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | ||
Theorem | biantru 527 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 26-May-1993.) |
⊢ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑)) | ||
Theorem | biantrur 528 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.) |
⊢ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓)) | ||
Theorem | biantrud 529 | 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 530 | A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒))) | ||
Theorem | mpbirand 531 | Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜃)) | ||
Theorem | jaao 532 | Inference conjoining and disjoining the antecedents of two implications. (Contributed by NM, 30-Sep-1999.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∨ 𝜏) → 𝜒)) | ||
Theorem | jaoa 533 | Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜒)) ⇒ ⊢ ((𝜑 ∨ 𝜃) → ((𝜓 ∧ 𝜏) → 𝜒)) | ||
Theorem | pm3.44 534 | Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) → ((𝜓 ∨ 𝜒) → 𝜑)) | ||
Theorem | jao 535 | Disjunction of antecedents. Compare Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 4-Apr-2013.) |
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜓) → ((𝜑 ∨ 𝜒) → 𝜓))) | ||
Theorem | pm1.2 536 | Axiom *1.2 of [WhiteheadRussell] p. 96, which they call "Taut". (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ 𝜑) → 𝜑) | ||
Theorem | oridm 537 | Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.) |
⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑) | ||
Theorem | pm4.25 538 | Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) |
⊢ (𝜑 ↔ (𝜑 ∨ 𝜑)) | ||
Theorem | orim12i 539 | Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)) | ||
Theorem | orim1i 540 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜒)) | ||
Theorem | orim2i 541 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) | ||
Theorem | orbi2i 542 | Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) | ||
Theorem | orbi1i 543 | Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) | ||
Theorem | orbi12i 544 | Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃)) | ||
Theorem | pm1.5 545 | Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜓 ∨ (𝜑 ∨ 𝜒))) | ||
Theorem | or12 546 | Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ (𝜓 ∨ (𝜑 ∨ 𝜒))) | ||
Theorem | orass 547 | Associative law for disjunction. Theorem *4.33 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | ||
Theorem | pm2.31 548 | Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → ((𝜑 ∨ 𝜓) ∨ 𝜒)) | ||
Theorem | pm2.32 549 | Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ (𝜓 ∨ 𝜒))) | ||
Theorem | or32 550 | A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜓)) | ||
Theorem | or4 551 | Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.) |
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜃))) | ||
Theorem | or42 552 | Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.) |
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜃 ∨ 𝜓))) | ||
Theorem | orordi 553 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜒))) | ||
Theorem | orordir 554 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜒))) | ||
Theorem | jca 555 | Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). Equivalent to the natural deduction rule ∧ I (∧ introduction), see natded 27571. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒)) | ||
Theorem | jcad 556 | Deduction conjoining the consequents of two implications. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) | ||
Theorem | jca2 557 | Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜓 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) | ||
Theorem | jca31 558 | Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) | ||
Theorem | jca32 559 | Join three consequents. (Contributed by FL, 1-Aug-2009.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃))) | ||
Theorem | jcai 560 | Deduction replacing implication with conjunction. (Contributed by NM, 15-Jul-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒)) | ||
Theorem | jctil 561 | Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 ⇒ ⊢ (𝜑 → (𝜒 ∧ 𝜓)) | ||
Theorem | jctir 562 | Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.) |
⊢ (𝜑 → 𝜓) & ⊢ 𝜒 ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒)) | ||
Theorem | jccir 563 | Inference conjoining a consequent of a consequent to the right of the consequent in an implication. See also ex-natded5.3i 27577. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by AV, 20-Aug-2019.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜓 → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒)) | ||
Theorem | jccil 564 | 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 555 (as done in jccir 563), 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 565 | 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 566 | 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 567 | Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒))) | ||
Theorem | jctird 568 | Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) | ||
Theorem | syl6an 569 | A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ ((𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜒 → 𝜏)) | ||
Theorem | ancl 570 | Conjoin antecedent to left of consequent. (Contributed by NM, 15-Aug-1994.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜑 ∧ 𝜓))) | ||
Theorem | anclb 571 | 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 | pm5.42 572 | Theorem *5.42 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))) | ||
Theorem | ancr 573 | Conjoin antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.) |
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜓 ∧ 𝜑))) | ||
Theorem | ancrb 574 | Conjoin antecedent to right of consequent. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜓 ∧ 𝜑))) | ||
Theorem | ancli 575 | Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜑 ∧ 𝜓)) | ||
Theorem | ancri 576 | Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜑)) | ||
Theorem | ancld 577 | 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 578 | 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 | anc2l 579 | 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 580 | Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜒 ∧ 𝜑)))) | ||
Theorem | anc2li 581 | 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 582 | 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 | pm3.41 583 | Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜒) → ((𝜑 ∧ 𝜓) → 𝜒)) | ||
Theorem | pm3.42 584 | Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜓 → 𝜒) → ((𝜑 ∧ 𝜓) → 𝜒)) | ||
Theorem | pm3.4 585 | Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113. (Contributed by NM, 31-Jul-1995.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜑 → 𝜓)) | ||
Theorem | pm4.45im 586 | Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.) |
⊢ (𝜑 ↔ (𝜑 ∧ (𝜓 → 𝜑))) | ||
Theorem | anim12d 587 | Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) | ||
Theorem | anim12d1 588 | Variant of anim12d 587 where the second implication does not depend on the antecedent. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → 𝜏) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) | ||
Theorem | anim1d 589 | Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃))) | ||
Theorem | anim2d 590 | Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒))) | ||
Theorem | anim12i 591 | Conjoin antecedents and consequents of two premises. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃)) | ||
Theorem | anim12ci 592 | Variant of anim12i 591 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜃 ∧ 𝜓)) | ||
Theorem | anim1i 593 | Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | ||
Theorem | anim2i 594 | Introduce conjunct to both sides of an implication. (Contributed by NM, 3-Jan-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓)) | ||
Theorem | anim12ii 595 | Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007.) (Proof shortened by Wolf Lammen, 19-Jul-2013.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜓 → 𝜏)) ⇒ ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → (𝜒 ∧ 𝜏))) | ||
Theorem | prth 596 | Conjoin antecedents and consequents of two premises. This is the closed theorem form of anim12d 587. Theorem *3.47 of [WhiteheadRussell] p. 113. It was proved by Leibniz, and it evidently pleased him enough to call it praeclarum theorema (splendid theorem). (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))) | ||
Theorem | pm2.3 597 | Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜑 ∨ (𝜒 ∨ 𝜓))) | ||
Theorem | pm2.41 598 | Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜓 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓)) | ||
Theorem | pm2.42 599 | Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
⊢ ((¬ 𝜑 ∨ (𝜑 → 𝜓)) → (𝜑 → 𝜓)) | ||
Theorem | pm2.4 600 | Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |