Home | Metamath
Proof Explorer Theorem List (p. 5 of 450) | < 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-28694) |
Hilbert Space Explorer
(28695-30217) |
Users' Mathboxes
(30218-44905) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pm4.67 401 | Theorem *4.67 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (¬ 𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∧ 𝜓)) | ||
Theorem | imnan 402 | Express an implication in terms of a negated conjunction. (Contributed by NM, 9-Apr-1994.) |
⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓)) | ||
Theorem | imnani 403 | Infer an implication from a negated conjunction. (Contributed by Mario Carneiro, 28-Sep-2015.) |
⊢ ¬ (𝜑 ∧ 𝜓) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | iman 404 | Implication in terms of conjunction and negation. Theorem 3.4(27) of [Stoll] p. 176. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2012.) |
⊢ ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) | ||
Theorem | pm3.24 405 | Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who call it the "law of contradiction"). (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ ¬ (𝜑 ∧ ¬ 𝜑) | ||
Theorem | annim 406 | Express a conjunction in terms of a negated implication. (Contributed by NM, 2-Aug-1994.) |
⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)) | ||
Theorem | pm4.61 407 | Theorem *4.61 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (𝜑 → 𝜓) ↔ (𝜑 ∧ ¬ 𝜓)) | ||
Theorem | pm4.65 408 | Theorem *4.65 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
⊢ (¬ (¬ 𝜑 → 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓)) | ||
Theorem | imp 409 | Importation inference. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | impcom 410 | Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) | ||
Theorem | con3dimp 411 | Variant of con3d 155 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓) | ||
Theorem | mpnanrd 412 | Eliminate the right side of a negated conjunction in an implication. (Contributed by ML, 17-Oct-2020.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | impd 413 | Importation deduction. (Contributed by NM, 31-Mar-1994.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | ||
Theorem | impcomd 414 | Importation deduction with commuted antecedents. (Contributed by Peter Mazsa, 24-Sep-2022.) (Proof shortened by Wolf Lammen, 22-Oct-2022.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃)) | ||
Theorem | ex 415 | Exportation inference. (This theorem used to be labeled "exp" but was changed to "ex" so as not to conflict with the math token "exp", per the June 2006 Metamath spec change.) A translation of natural deduction rule → I (→ introduction), see natded 28181. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | expcom 416 | Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜓 → (𝜑 → 𝜒)) | ||
Theorem | expdcom 417 | Commuted form of expd 418. (Contributed by Alan Sare, 18-Mar-2012.) Shorten expd 418. (Revised by Wolf Lammen, 28-Jul-2022.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜓 → (𝜒 → (𝜑 → 𝜃))) | ||
Theorem | expd 418 | Exportation deduction. (Contributed by NM, 20-Aug-1993.) (Proof shortened by Wolf Lammen, 28-Jul-2022.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | ||
Theorem | expcomd 419 | Deduction form of expcom 416. (Contributed by Alan Sare, 22-Jul-2012.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → (𝜒 → (𝜓 → 𝜃))) | ||
Theorem | imp31 420 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | imp32 421 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | ||
Theorem | exp31 422 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | ||
Theorem | exp32 423 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | ||
Theorem | imp4b 424 | An importation inference. (Contributed by NM, 26-Apr-1994.) Shorten imp4a 425. (Revised by Wolf Lammen, 19-Jul-2021.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) | ||
Theorem | imp4a 425 | An importation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Jul-2021.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))) | ||
Theorem | imp4c 426 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)) | ||
Theorem | imp4d 427 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ (𝜑 → ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)) | ||
Theorem | imp41 428 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) | ||
Theorem | imp42 429 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏) | ||
Theorem | imp43 430 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) | ||
Theorem | imp44 431 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏) | ||
Theorem | imp45 432 | An importation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜏) | ||
Theorem | exp4b 433 | An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) Shorten exp4a 434. (Revised by Wolf Lammen, 20-Jul-2021.) |
⊢ ((𝜑 ∧ 𝜓) → ((𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | ||
Theorem | exp4a 434 | An exportation inference. (Contributed by NM, 26-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jul-2021.) |
⊢ (𝜑 → (𝜓 → ((𝜒 ∧ 𝜃) → 𝜏))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | ||
Theorem | exp4c 435 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | ||
Theorem | exp4d 436 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (𝜑 → ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | ||
Theorem | exp41 437 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | ||
Theorem | exp42 438 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | ||
Theorem | exp43 439 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | ||
Theorem | exp44 440 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ ((𝜑 ∧ ((𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | ||
Theorem | exp45 441 | An exportation inference. (Contributed by NM, 26-Apr-1994.) |
⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | ||
Theorem | imp5d 442 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂)) | ||
Theorem | imp5a 443 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) (Proof shortened by Wolf Lammen, 2-Aug-2022.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → ((𝜃 ∧ 𝜏) → 𝜂)))) | ||
Theorem | imp5g 444 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (((𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂)) | ||
Theorem | imp55 445 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) ⇒ ⊢ (((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) ∧ 𝜏) → 𝜂) | ||
Theorem | imp511 446 | An importation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) ⇒ ⊢ ((𝜑 ∧ ((𝜓 ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏)) → 𝜂) | ||
Theorem | exp5c 447 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | ||
Theorem | exp5j 448 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ (𝜑 → ((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | ||
Theorem | exp5l 449 | An exportation inference. (Contributed by Jeff Hankins, 7-Jul-2009.) |
⊢ (𝜑 → (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | ||
Theorem | exp53 450 | An exportation inference. (Contributed by Jeff Hankins, 30-Aug-2009.) |
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) | ||
Theorem | pm3.3 451 | Theorem *3.3 (Exp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) | ||
Theorem | pm3.31 452 | Theorem *3.31 (Imp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒)) | ||
Theorem | impexp 453 | Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.) |
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) | ||
Theorem | impancom 454 | Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃)) | ||
Theorem | expdimp 455 | A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) | ||
Theorem | expimpd 456 | Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | ||
Theorem | impr 457 | Import a wff into a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | ||
Theorem | impl 458 | Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | expr 459 | Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) | ||
Theorem | expl 460 | Export a wff from a left conjunct. (Contributed by Jeff Hankins, 28-Aug-2009.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | ||
Theorem | ancoms 461 | Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) | ||
Theorem | pm3.22 462 | Theorem *3.22 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑)) | ||
Theorem | ancom 463 | Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.) |
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | ||
Theorem | ancomd 464 | Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 ∧ 𝜓)) | ||
Theorem | biancomi 465 | Commuting conjunction in a biconditional. (Contributed by Peter Mazsa, 17-Jun-2018.) |
⊢ (𝜑 ↔ (𝜒 ∧ 𝜓)) ⇒ ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) | ||
Theorem | biancomd 466 | Commuting conjunction in a biconditional, deduction form. (Contributed by Peter Mazsa, 3-Oct-2018.) |
⊢ (𝜑 → (𝜓 ↔ (𝜃 ∧ 𝜒))) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) | ||
Theorem | ancomst 467 | Closed form of ancoms 461. (Contributed by Alan Sare, 31-Dec-2011.) |
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜓 ∧ 𝜑) → 𝜒)) | ||
Theorem | ancomsd 468 | Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃)) | ||
Theorem | anasss 469 | Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | ||
Theorem | anassrs 470 | Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | anass 471 | Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | ||
Theorem | pm3.2 472 | Join antecedents with conjunction ("conjunction introduction"). Theorem *3.2 of [WhiteheadRussell] p. 111. Its associated inference is pm3.2i 473 and its associated deduction is jca 514 (and the double deduction is jcad 515). See pm3.2im 162 for a version using only implication and negation. (Contributed by NM, 5-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) |
⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓))) | ||
Theorem | pm3.2i 473 | Infer conjunction of premises. Inference associated with pm3.2 472. Its associated deduction is jca 514 (and the double deduction is jcad 515). (Contributed by NM, 21-Jun-1993.) |
⊢ 𝜑 & ⊢ 𝜓 ⇒ ⊢ (𝜑 ∧ 𝜓) | ||
Theorem | pm3.21 474 | Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑))) | ||
Theorem | pm3.43i 475 | Nested conjunction of antecedents. (Contributed by NM, 4-Jan-1993.) |
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜒) → (𝜑 → (𝜓 ∧ 𝜒)))) | ||
Theorem | pm3.43 476 | Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ∧ 𝜒))) | ||
Theorem | dfbi2 477 | A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 24-Jan-1993.) |
⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) | ||
Theorem | dfbi 478 | Definition df-bi 209 rewritten in an abbreviated form to help intuitive understanding of that definition. Note that it is a conjunction of two implications; one which asserts properties that follow from the biconditional and one which asserts properties that imply the biconditional. (Contributed by NM, 15-Aug-2008.) |
⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) | ||
Theorem | biimpa 479 | Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | biimpar 480 | Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜓) | ||
Theorem | biimpac 481 | Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) | ||
Theorem | biimparc 482 | Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜒 ∧ 𝜑) → 𝜓) | ||
Theorem | adantr 483 | Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜓) | ||
Theorem | adantl 484 | Inference adding a conjunct to the left of an antecedent. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Nov-2012.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑) → 𝜓) | ||
Theorem | simpl 485 | Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜑) | ||
Theorem | simpli 486 | Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.) |
⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ 𝜑 | ||
Theorem | simpr 487 | Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜓) | ||
Theorem | simpri 488 | Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.) |
⊢ (𝜑 ∧ 𝜓) ⇒ ⊢ 𝜓 | ||
Theorem | intnan 489 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.) |
⊢ ¬ 𝜑 ⇒ ⊢ ¬ (𝜓 ∧ 𝜑) | ||
Theorem | intnanr 490 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.) |
⊢ ¬ 𝜑 ⇒ ⊢ ¬ (𝜑 ∧ 𝜓) | ||
Theorem | intnand 491 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓)) | ||
Theorem | intnanrd 492 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) | ||
Theorem | adantld 493 | Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜒)) | ||
Theorem | adantrd 494 | Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒)) | ||
Theorem | pm3.41 495 | Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜑 → 𝜒) → ((𝜑 ∧ 𝜓) → 𝜒)) | ||
Theorem | pm3.42 496 | Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) |
⊢ ((𝜓 → 𝜒) → ((𝜑 ∧ 𝜓) → 𝜒)) | ||
Theorem | simpld 497 | Deduction eliminating a conjunct. A translation of natural deduction rule ∧ EL (∧ elimination left), see natded 28181. (Contributed by NM, 26-May-1993.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | simprd 498 | Deduction eliminating a conjunct. (Contributed by NM, 14-May-1993.) A translation of natural deduction rule ∧ ER (∧ elimination right), see natded 28181. (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | simprbi 499 | Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | simplbi 500 | Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |