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