HomeHome Intuitionistic Logic Explorer
Theorem List (p. 6 of 105)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 501-600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorempm4.87 501 Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Eric Schmidt, 26-Oct-2006.)
 |-  ( ( ( ( ( ph  /\  ps )  ->  ch )  <->  ( ph  ->  ( ps  ->  ch )
 ) )  /\  (
 ( ph  ->  ( ps 
 ->  ch ) )  <->  ( ps  ->  (
 ph  ->  ch ) ) ) )  /\  ( ( ps  ->  ( ph  ->  ch ) )  <->  ( ( ps 
 /\  ph )  ->  ch )
 ) )
 
Theoremabai 502 Introduce one conjunct as an antecedent to the other. "abai" stands for "and, biconditional, and, implication". (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
 |-  ( ( ph  /\  ps ) 
 <->  ( ph  /\  ( ph  ->  ps ) ) )
 
Theoreman12 503 Swap two conjuncts. Note that the first digit (1) in the label refers to the outer conjunct position, and the next digit (2) to the inner conjunct position. (Contributed by NM, 12-Mar-1995.)
 |-  ( ( ph  /\  ( ps  /\  ch ) )  <-> 
 ( ps  /\  ( ph  /\  ch ) ) )
 
Theoreman32 504 A rearrangement of conjuncts. (Contributed by NM, 12-Mar-1995.) (Proof shortened by Wolf Lammen, 25-Dec-2012.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ch ) 
 <->  ( ( ph  /\  ch )  /\  ps ) )
 
Theoreman13 505 A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
 |-  ( ( ph  /\  ( ps  /\  ch ) )  <-> 
 ( ch  /\  ( ps  /\  ph ) ) )
 
Theoreman31 506 A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ch ) 
 <->  ( ( ch  /\  ps )  /\  ph )
 )
 
Theoreman12s 507 Swap two conjuncts in antecedent. The label suffix "s" means that an12 503 is combined with syl 14 (or a variant). (Contributed by NM, 13-Mar-1996.)
 |-  ( ( ph  /\  ( ps  /\  ch ) ) 
 ->  th )   =>    |-  ( ( ps  /\  ( ph  /\  ch )
 )  ->  th )
 
Theoremancom2s 508 Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
 |-  ( ( ph  /\  ( ps  /\  ch ) ) 
 ->  th )   =>    |-  ( ( ph  /\  ( ch  /\  ps ) ) 
 ->  th )
 
Theoreman13s 509 Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
 |-  ( ( ph  /\  ( ps  /\  ch ) ) 
 ->  th )   =>    |-  ( ( ch  /\  ( ps  /\  ph )
 )  ->  th )
 
Theoreman32s 510 Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ch )  ->  th )   =>    |-  ( ( ( ph  /\ 
 ch )  /\  ps )  ->  th )
 
Theoremancom1s 511 Inference commuting a nested conjunction in antecedent. (Contributed by NM, 24-May-2006.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ch )  ->  th )   =>    |-  ( ( ( ps 
 /\  ph )  /\  ch )  ->  th )
 
Theoreman31s 512 Swap two conjuncts in antecedent. (Contributed by NM, 31-May-2006.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ch )  ->  th )   =>    |-  ( ( ( ch 
 /\  ps )  /\  ph )  ->  th )
 
Theoremanass1rs 513 Commutative-associative law for conjunction in an antecedent. (Contributed by Jeff Madsen, 19-Jun-2011.)
 |-  ( ( ph  /\  ( ps  /\  ch ) ) 
 ->  th )   =>    |-  ( ( ( ph  /\ 
 ch )  /\  ps )  ->  th )
 
Theoremanabs1 514 Absorption into embedded conjunct. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Wolf Lammen, 16-Nov-2013.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ph )  <->  (
 ph  /\  ps )
 )
 
Theoremanabs5 515 Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
 |-  ( ( ph  /\  ( ph  /\  ps ) )  <-> 
 ( ph  /\  ps )
 )
 
Theoremanabs7 516 Absorption into embedded conjunct. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 17-Nov-2013.)
 |-  ( ( ps  /\  ( ph  /\  ps )
 ) 
 <->  ( ph  /\  ps ) )
 
Theoremanabsan 517 Absorption of antecedent with conjunction. (Contributed by NM, 24-Mar-1996.) (Revised by NM, 18-Nov-2013.)
 |-  ( ( ( ph  /\  ph )  /\  ps )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
Theoremanabss1 518 Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ph )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
Theoremanabss4 519 Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.)
 |-  ( ( ( ps 
 /\  ph )  /\  ps )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
Theoremanabss5 520 Absorption of antecedent into conjunction. (Contributed by NM, 10-May-1994.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
 |-  ( ( ph  /\  ( ph  /\  ps ) ) 
 ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
Theoremanabsi5 521 Absorption of antecedent into conjunction. (Contributed by NM, 11-Jun-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
 |-  ( ph  ->  (
 ( ph  /\  ps )  ->  ch ) )   =>    |-  ( ( ph  /\ 
 ps )  ->  ch )
 
Theoremanabsi6 522 Absorption of antecedent into conjunction. (Contributed by NM, 14-Aug-2000.)
 |-  ( ph  ->  (
 ( ps  /\  ph )  ->  ch ) )   =>    |-  ( ( ph  /\ 
 ps )  ->  ch )
 
Theoremanabsi7 523 Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 18-Nov-2013.)
 |-  ( ps  ->  (
 ( ph  /\  ps )  ->  ch ) )   =>    |-  ( ( ph  /\ 
 ps )  ->  ch )
 
Theoremanabsi8 524 Absorption of antecedent into conjunction. (Contributed by NM, 26-Sep-1999.)
 |-  ( ps  ->  (
 ( ps  /\  ph )  ->  ch ) )   =>    |-  ( ( ph  /\ 
 ps )  ->  ch )
 
Theoremanabss7 525 Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 19-Nov-2013.)
 |-  ( ( ps  /\  ( ph  /\  ps )
 )  ->  ch )   =>    |-  (
 ( ph  /\  ps )  ->  ch )
 
Theoremanabsan2 526 Absorption of antecedent with conjunction. (Contributed by NM, 10-May-2004.) (Revised by NM, 1-Jan-2013.)
 |-  ( ( ph  /\  ( ps  /\  ps ) ) 
 ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
Theoremanabss3 527 Absorption of antecedent into conjunction. (Contributed by NM, 20-Jul-1996.) (Proof shortened by Wolf Lammen, 1-Jan-2013.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ps )  ->  ch )   =>    |-  ( ( ph  /\  ps )  ->  ch )
 
Theoreman4 528 Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ( ch  /\  th ) )  <-> 
 ( ( ph  /\  ch )  /\  ( ps  /\  th ) ) )
 
Theoreman42 529 Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ( ch  /\  th ) )  <-> 
 ( ( ph  /\  ch )  /\  ( th  /\  ps ) ) )
 
Theoreman4s 530 Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ( ch  /\  th ) ) 
 ->  ta )   =>    |-  ( ( ( ph  /\ 
 ch )  /\  ( ps  /\  th ) ) 
 ->  ta )
 
Theoreman42s 531 Inference rearranging 4 conjuncts in antecedent. (Contributed by NM, 10-Aug-1995.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ( ch  /\  th ) ) 
 ->  ta )   =>    |-  ( ( ( ph  /\ 
 ch )  /\  ( th  /\  ps ) ) 
 ->  ta )
 
Theoremanandi 532 Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)
 |-  ( ( ph  /\  ( ps  /\  ch ) )  <-> 
 ( ( ph  /\  ps )  /\  ( ph  /\  ch ) ) )
 
Theoremanandir 533 Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ch ) 
 <->  ( ( ph  /\  ch )  /\  ( ps  /\  ch ) ) )
 
Theoremanandis 534 Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
 |-  ( ( ( ph  /\ 
 ps )  /\  ( ph  /\  ch ) ) 
 ->  ta )   =>    |-  ( ( ph  /\  ( ps  /\  ch ) ) 
 ->  ta )
 
Theoremanandirs 535 Inference that undistributes conjunction in the antecedent. (Contributed by NM, 7-Jun-2004.)
 |-  ( ( ( ph  /\ 
 ch )  /\  ( ps  /\  ch ) ) 
 ->  ta )   =>    |-  ( ( ( ph  /\ 
 ps )  /\  ch )  ->  ta )
 
Theoremsyl2an2 536 syl2an 277 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
 |-  ( ph  ->  ps )   &    |-  (
 ( ch  /\  ph )  ->  th )   &    |-  ( ( ps 
 /\  th )  ->  ta )   =>    |-  (
 ( ch  /\  ph )  ->  ta )
 
Theoremsyl2an2r 537 syl2anr 278 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
 |-  ( ph  ->  ps )   &    |-  (
 ( ph  /\  ch )  ->  th )   &    |-  ( ( ps 
 /\  th )  ->  ta )   =>    |-  (
 ( ph  /\  ch )  ->  ta )
 
Theoremimpbida 538 Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.)
 |-  ( ( ph  /\  ps )  ->  ch )   &    |-  ( ( ph  /\ 
 ch )  ->  ps )   =>    |-  ( ph  ->  ( ps  <->  ch ) )
 
Theorempm3.45 539 Theorem *3.45 (Fact) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
 |-  ( ( ph  ->  ps )  ->  ( ( ph  /\  ch )  ->  ( ps  /\  ch )
 ) )
 
Theoremim2anan9 540 Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
 |-  ( ph  ->  ( ps  ->  ch ) )   &    |-  ( th  ->  ( ta  ->  et ) )   =>    |-  ( ( ph  /\  th )  ->  ( ( ps 
 /\  ta )  ->  ( ch  /\  et ) ) )
 
Theoremim2anan9r 541 Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)
 |-  ( ph  ->  ( ps  ->  ch ) )   &    |-  ( th  ->  ( ta  ->  et ) )   =>    |-  ( ( th  /\  ph )  ->  ( ( ps  /\  ta )  ->  ( ch  /\  et )
 ) )
 
Theoremanim12dan 542 Conjoin antecedents and consequents in a deduction. (Contributed by Mario Carneiro, 12-May-2014.)
 |-  ( ( ph  /\  ps )  ->  ch )   &    |-  ( ( ph  /\ 
 th )  ->  ta )   =>    |-  (
 ( ph  /\  ( ps 
 /\  th ) )  ->  ( ch  /\  ta )
 )
 
Theorempm5.1 543 Two propositions are equivalent if they are both true. Theorem *5.1 of [WhiteheadRussell] p. 123. (Contributed by NM, 21-May-1994.)
 |-  ( ( ph  /\  ps )  ->  ( ph  <->  ps ) )
 
Theorempm3.43 544 Theorem *3.43 (Comp) of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 27-Nov-2013.)
 |-  ( ( ( ph  ->  ps )  /\  ( ph  ->  ch ) )  ->  ( ph  ->  ( ps  /\ 
 ch ) ) )
 
Theoremjcab 545 Distributive law for implication over conjunction. Compare Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 27-Nov-2013.)
 |-  ( ( ph  ->  ( ps  /\  ch )
 ) 
 <->  ( ( ph  ->  ps )  /\  ( ph  ->  ch ) ) )
 
Theorempm4.76 546 Theorem *4.76 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
 |-  ( ( ( ph  ->  ps )  /\  ( ph  ->  ch ) )  <->  ( ph  ->  ( ps  /\  ch )
 ) )
 
Theorempm4.38 547 Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
 |-  ( ( ( ph  <->  ch )  /\  ( ps  <->  th ) )  ->  ( ( ph  /\  ps ) 
 <->  ( ch  /\  th ) ) )
 
Theorembi2anan9 548 Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)
 |-  ( ph  ->  ( ps 
 <->  ch ) )   &    |-  ( th  ->  ( ta  <->  et ) )   =>    |-  ( ( ph  /\ 
 th )  ->  (
 ( ps  /\  ta ) 
 <->  ( ch  /\  et ) ) )
 
Theorembi2anan9r 549 Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.)
 |-  ( ph  ->  ( ps 
 <->  ch ) )   &    |-  ( th  ->  ( ta  <->  et ) )   =>    |-  ( ( th  /\  ph )  ->  ( ( ps  /\  ta )  <->  ( ch  /\  et )
 ) )
 
Theorembi2bian9 550 Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004.)
 |-  ( ph  ->  ( ps 
 <->  ch ) )   &    |-  ( th  ->  ( ta  <->  et ) )   =>    |-  ( ( ph  /\ 
 th )  ->  (
 ( ps  <->  ta )  <->  ( ch  <->  et ) ) )
 
Theorempm5.33 551 Theorem *5.33 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
 |-  ( ( ph  /\  ( ps  ->  ch ) )  <->  ( ph  /\  (
 ( ph  /\  ps )  ->  ch ) ) )
 
Theorempm5.36 552 Theorem *5.36 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
 |-  ( ( ph  /\  ( ph 
 <->  ps ) )  <->  ( ps  /\  ( ph  <->  ps ) ) )
 
Theorembianabs 553 Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.)
 |-  ( ph  ->  ( ps 
 <->  ( ph  /\  ch ) ) )   =>    |-  ( ph  ->  ( ps  <->  ch ) )
 
1.2.5  Logical negation (intuitionistic)
 
Axiomax-in1 554 'Not' introduction. One of the axioms of propositional logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
 |-  ( ( ph  ->  -.  ph )  ->  -.  ph )
 
Axiomax-in2 555 'Not' elimination. One of the axioms of propositional logic. (Contributed by Mario Carneiro, 31-Jan-2015.)
 |-  ( -.  ph  ->  (
 ph  ->  ps ) )
 
Theorempm2.01 556 Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. This is valid intuitionistically (in the terminology of Section 1.2 of [Bauer] p. 482 it is a proof of negation not a proof by contradiction); compare with pm2.18dc 761 which only holds for some propositions. (Contributed by Mario Carneiro, 12-May-2015.)
 |-  ( ( ph  ->  -.  ph )  ->  -.  ph )
 
Theorempm2.21 557 From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. (Contributed by Mario Carneiro, 12-May-2015.)
 |-  ( -.  ph  ->  (
 ph  ->  ps ) )
 
Theorempm2.01d 558 Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
 |-  ( ph  ->  ( ps  ->  -.  ps )
 )   =>    |-  ( ph  ->  -.  ps )
 
Theorempm2.21d 559 A contradiction implies anything. Deduction from pm2.21 557. (Contributed by NM, 10-Feb-1996.)
 |-  ( ph  ->  -.  ps )   =>    |-  ( ph  ->  ( ps  ->  ch ) )
 
Theorempm2.21dd 560 A contradiction implies anything. Deduction from pm2.21 557. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ph  ->  ps )   &    |-  ( ph  ->  -.  ps )   =>    |-  ( ph  ->  ch )
 
Theorempm2.24 561 Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
 |-  ( ph  ->  ( -.  ph  ->  ps )
 )
 
Theorempm2.24d 562 Deduction version of pm2.24 561. (Contributed by NM, 30-Jan-2006.) (Revised by Mario Carneiro, 31-Jan-2015.)
 |-  ( ph  ->  ps )   =>    |-  ( ph  ->  ( -.  ps  ->  ch ) )
 
Theorempm2.24i 563 Inference version of pm2.24 561. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 31-Jan-2015.)
 |-  ph   =>    |-  ( -.  ph  ->  ps )
 
Theoremcon2d 564 A contraposition deduction. (Contributed by NM, 19-Aug-1993.) (Revised by NM, 12-Feb-2013.)
 |-  ( ph  ->  ( ps  ->  -.  ch )
 )   =>    |-  ( ph  ->  ( ch  ->  -.  ps )
 )
 
Theoremmt2d 565 Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)
 |-  ( ph  ->  ch )   &    |-  ( ph  ->  ( ps  ->  -. 
 ch ) )   =>    |-  ( ph  ->  -. 
 ps )
 
Theoremnsyl3 566 A negated syllogism inference. (Contributed by NM, 1-Dec-1995.) (Revised by NM, 13-Jun-2013.)
 |-  ( ph  ->  -.  ps )   &    |-  ( ch  ->  ps )   =>    |-  ( ch  ->  -.  ph )
 
Theoremcon2i 567 A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.)
 |-  ( ph  ->  -.  ps )   =>    |-  ( ps  ->  -.  ph )
 
Theoremnsyl 568 A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
 |-  ( ph  ->  -.  ps )   &    |-  ( ch  ->  ps )   =>    |-  ( ph  ->  -.  ch )
 
Theoremnotnot 569 Double negation introduction. Theorem *2.12 of [WhiteheadRussell] p. 101. This one holds for all propositions, but its converse only holds for decidable propositions (see notnotrdc 762). (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
 |-  ( ph  ->  -.  -.  ph )
 
Theoremnotnotd 570 Deduction associated with notnot 569 and notnoti 584. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.)
 |-  ( ph  ->  ps )   =>    |-  ( ph  ->  -.  -.  ps )
 
Theoremcon3d 571 A contraposition deduction. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 31-Jan-2015.)
 |-  ( ph  ->  ( ps  ->  ch ) )   =>    |-  ( ph  ->  ( -.  ch  ->  -.  ps ) )
 
Theoremcon3i 572 A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)
 |-  ( ph  ->  ps )   =>    |-  ( -.  ps  ->  -.  ph )
 
Theoremcon3rr3 573 Rotate through consequent right. (Contributed by Wolf Lammen, 3-Nov-2013.)
 |-  ( ph  ->  ( ps  ->  ch ) )   =>    |-  ( -.  ch  ->  ( ph  ->  -.  ps ) )
 
Theoremcon3dimp 574 Variant of con3d 571 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
 |-  ( ph  ->  ( ps  ->  ch ) )   =>    |-  ( ( ph  /\ 
 -.  ch )  ->  -.  ps )
 
Theorempm2.01da 575 Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
 |-  ( ( ph  /\  ps )  ->  -.  ps )   =>    |-  ( ph  ->  -.  ps )
 
Theorempm3.2im 576 In classical logic, this is just a restatement of pm3.2 130. In intuitionistic logic, it still holds, but is weaker than pm3.2. (Contributed by Mario Carneiro, 12-May-2015.)
 |-  ( ph  ->  ( ps  ->  -.  ( ph  ->  -.  ps ) ) )
 
Theoremexpi 577 An exportation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.)
 |-  ( -.  ( ph  ->  -.  ps )  ->  ch )   =>    |-  ( ph  ->  ( ps  ->  ch ) )
 
Theorempm2.65i 578 Inference rule for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
 |-  ( ph  ->  ps )   &    |-  ( ph  ->  -.  ps )   =>    |-  -.  ph
 
Theoremmt2 579 A rule similar to modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Sep-2013.)
 |- 
 ps   &    |-  ( ph  ->  -.  ps )   =>    |- 
 -.  ph
 
Theorembiijust 580 Theorem used to justify definition of intuitionistic biconditional df-bi 114. (Contributed by NM, 24-Nov-2017.)
 |-  ( ( ( (
 ph  ->  ps )  /\  ( ps  ->  ph ) )  ->  ( ( ph  ->  ps )  /\  ( ps 
 ->  ph ) ) ) 
 /\  ( ( (
 ph  ->  ps )  /\  ( ps  ->  ph ) )  ->  ( ( ph  ->  ps )  /\  ( ps 
 ->  ph ) ) ) )
 
Theoremcon3 581 Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)
 |-  ( ( ph  ->  ps )  ->  ( -.  ps 
 ->  -.  ph ) )
 
Theoremcon2 582 Contraposition. Theorem *2.03 of [WhiteheadRussell] p. 100. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)
 |-  ( ( ph  ->  -. 
 ps )  ->  ( ps  ->  -.  ph ) )
 
Theoremmt2i 583 Modus tollens inference. (Contributed by NM, 26-Mar-1995.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
 |- 
 ch   &    |-  ( ph  ->  ( ps  ->  -.  ch )
 )   =>    |-  ( ph  ->  -.  ps )
 
Theoremnotnoti 584 Infer double negation. (Contributed by NM, 27-Feb-2008.)
 |-  ph   =>    |- 
 -.  -.  ph
 
Theorempm2.21i 585 A contradiction implies anything. Inference from pm2.21 557. (Contributed by NM, 16-Sep-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
 |- 
 -.  ph   =>    |-  ( ph  ->  ps )
 
Theorempm2.24ii 586 A contradiction implies anything. Inference from pm2.24 561. (Contributed by NM, 27-Feb-2008.)
 |-  ph   &    |- 
 -.  ph   =>    |- 
 ps
 
Theoremnsyld 587 A negated syllogism deduction. (Contributed by NM, 9-Apr-2005.)
 |-  ( ph  ->  ( ps  ->  -.  ch )
 )   &    |-  ( ph  ->  ( ta  ->  ch ) )   =>    |-  ( ph  ->  ( ps  ->  -.  ta )
 )
 
Theoremnsyli 588 A negated syllogism inference. (Contributed by NM, 3-May-1994.)
 |-  ( ph  ->  ( ps  ->  ch ) )   &    |-  ( th  ->  -.  ch )   =>    |-  ( ph  ->  ( th  ->  -. 
 ps ) )
 
Theoremmth8 589 Theorem 8 of [Margaris] p. 60. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)
 |-  ( ph  ->  ( -.  ps  ->  -.  ( ph  ->  ps ) ) )
 
Theoremjc 590 Inference joining the consequents of two premises. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  ->  ps )   &    |-  ( ph  ->  ch )   =>    |-  ( ph  ->  -.  ( ps  ->  -.  ch )
 )
 
Theorempm2.51 591 Theorem *2.51 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
 |-  ( -.  ( ph  ->  ps )  ->  ( ph  ->  -.  ps )
 )
 
Theorempm2.52 592 Theorem *2.52 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
 |-  ( -.  ( ph  ->  ps )  ->  ( -.  ph  ->  -.  ps )
 )
 
Theoremexpt 593 Exportation theorem expressed with primitive connectives. (Contributed by NM, 5-Aug-1993.)
 |-  ( ( -.  ( ph  ->  -.  ps )  ->  ch )  ->  ( ph  ->  ( ps  ->  ch ) ) )
 
Theoremjarl 594 Elimination of a nested antecedent. (Contributed by Wolf Lammen, 10-May-2013.)
 |-  ( ( ( ph  ->  ps )  ->  ch )  ->  ( -.  ph  ->  ch ) )
 
Theorempm2.65 595 Theorem *2.65 of [WhiteheadRussell] p. 107. Proof by contradiction. Proofs, such as this one, which assume a proposition, here  ph, derive a contradiction, and therefore conclude  -. 
ph, are valid intuitionistically (and can be called "proof of negation", for example by Section 1.2 of [Bauer] p. 482). By contrast, proofs which assume  -.  ph, derive a contradiction, and conclude  ph, such as condandc 786, are only valid for decidable propositions. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Mar-2013.)
 |-  ( ( ph  ->  ps )  ->  ( ( ph  ->  -.  ps )  ->  -.  ph ) )
 
Theorempm2.65d 596 Deduction rule for proof by contradiction. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 26-May-2013.)
 |-  ( ph  ->  ( ps  ->  ch ) )   &    |-  ( ph  ->  ( ps  ->  -. 
 ch ) )   =>    |-  ( ph  ->  -. 
 ps )
 
Theorempm2.65da 597 Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
 |-  ( ( ph  /\  ps )  ->  ch )   &    |-  ( ( ph  /\ 
 ps )  ->  -.  ch )   =>    |-  ( ph  ->  -.  ps )
 
Theoremmto 598 The rule of modus tollens. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
 |- 
 -.  ps   &    |-  ( ph  ->  ps )   =>    |- 
 -.  ph
 
Theoremmtod 599 Modus tollens deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)
 |-  ( ph  ->  -.  ch )   &    |-  ( ph  ->  ( ps  ->  ch ) )   =>    |-  ( ph  ->  -. 
 ps )
 
Theoremmtoi 600 Modus tollens inference. (Contributed by NM, 5-Jul-1994.) (Proof shortened by Wolf Lammen, 15-Sep-2012.)
 |- 
 -.  ch   &    |-  ( ph  ->  ( ps  ->  ch )
 )   =>    |-  ( ph  ->  -.  ps )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10490
  Copyright terms: Public domain < Previous  Next >