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