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