HomeHome Intuitionistic Logic Explorer
Theorem List (p. 9 of 114)
< 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 - 801-900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremcon34bdc 801 Contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116, but for a decidable proposition. (Contributed by Jim Kingdon, 24-Apr-2018.)
 |-  (DECID 
 ps  ->  ( ( ph  ->  ps )  <->  ( -.  ps  ->  -.  ph ) ) )
 
Theoremnotnotbdc 802 Double negation equivalence for a decidable proposition. Like Theorem *4.13 of [WhiteheadRussell] p. 117, but with a decidability antecendent. The forward direction, notnot 592, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 13-Mar-2018.)
 |-  (DECID 
 ph  ->  ( ph  <->  -.  -.  ph )
 )
 
Theoremcon1biimdc 803 Contraposition. (Contributed by Jim Kingdon, 4-Apr-2018.)
 |-  (DECID 
 ph  ->  ( ( -.  ph 
 <->  ps )  ->  ( -.  ps  <->  ph ) ) )
 
Theoremcon1bidc 804 Contraposition. (Contributed by Jim Kingdon, 17-Apr-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  ->  ( ( -.  ph 
 <->  ps )  <->  ( -.  ps  <->  ph ) ) ) )
 
Theoremcon2bidc 805 Contraposition. (Contributed by Jim Kingdon, 17-Apr-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  ->  ( ( ph  <->  -.  ps )  <->  ( ps  <->  -.  ph ) ) ) )
 
Theoremcon1biddc 806 A contraposition deduction. (Contributed by Jim Kingdon, 4-Apr-2018.)
 |-  ( ph  ->  (DECID  ps  ->  ( -.  ps  <->  ch ) ) )   =>    |-  ( ph  ->  (DECID  ps  ->  ( -.  ch  <->  ps ) ) )
 
Theoremcon1biidc 807 A contraposition inference. (Contributed by Jim Kingdon, 15-Mar-2018.)
 |-  (DECID 
 ph  ->  ( -.  ph  <->  ps ) )   =>    |-  (DECID 
 ph  ->  ( -.  ps  <->  ph ) )
 
Theoremcon1bdc 808 Contraposition. Bidirectional version of con1dc 789. (Contributed by NM, 5-Aug-1993.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  ->  ( ( -.  ph  ->  ps )  <->  ( -.  ps  -> 
 ph ) ) ) )
 
Theoremcon2biidc 809 A contraposition inference. (Contributed by Jim Kingdon, 15-Mar-2018.)
 |-  (DECID 
 ps  ->  ( ph  <->  -.  ps ) )   =>    |-  (DECID  ps  ->  ( ps  <->  -.  ph ) )
 
Theoremcon2biddc 810 A contraposition deduction. (Contributed by Jim Kingdon, 11-Apr-2018.)
 |-  ( ph  ->  (DECID  ch  ->  ( ps  <->  -.  ch ) ) )   =>    |-  ( ph  ->  (DECID  ch  ->  ( ch  <->  -.  ps ) ) )
 
Theoremcondandc 811 Proof by contradiction. This only holds for decidable propositions, as it is part of the family of theorems which assume  -.  ps, derive a contradiction, and therefore conclude  ps. By contrast, assuming  ps, deriving a contradiction, and therefore concluding  -.  ps, as in pm2.65 618, is valid for all propositions. (Contributed by Jim Kingdon, 13-May-2018.)
 |-  ( ( ph  /\  -.  ps )  ->  ch )   &    |-  (
 ( ph  /\  -.  ps )  ->  -.  ch )   =>    |-  (DECID  ps  ->  ( ph  ->  ps )
 )
 
Theorembijadc 812 Combine antecedents into a single biconditional. This inference is reminiscent of jadc 796. (Contributed by Jim Kingdon, 4-May-2018.)
 |-  ( ph  ->  ( ps  ->  ch ) )   &    |-  ( -.  ph  ->  ( -.  ps 
 ->  ch ) )   =>    |-  (DECID 
 ps  ->  ( ( ph  <->  ps )  ->  ch ) )
 
Theorempm5.18dc 813 Relationship between an equivalence and an equivalence with some negation, for decidable propositions. Based on theorem *5.18 of [WhiteheadRussell] p. 124. Given decidability, we can consider  -.  ( ph  <->  -.  ps ) to represent "negated exclusive-or". (Contributed by Jim Kingdon, 4-Apr-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  ->  ( ( ph  <->  ps ) 
 <->  -.  ( ph  <->  -.  ps ) ) ) )
 
Theoremdfandc 814 Definition of 'and' in terms of negation and implication, for decidable propositions. The forward direction holds for all propositions, and can (basically) be found at pm3.2im 599. (Contributed by Jim Kingdon, 30-Apr-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  ->  ( ( ph  /\ 
 ps )  <->  -.  ( ph  ->  -. 
 ps ) ) ) )
 
Theorempm2.13dc 815 A decidable proposition or its triple negation is true. Theorem *2.13 of [WhiteheadRussell] p. 101 with decidability condition added. (Contributed by Jim Kingdon, 13-May-2018.)
 |-  (DECID 
 ph  ->  ( ph  \/  -. 
 -.  -.  ph ) )
 
Theorempm4.63dc 816 Theorem *4.63 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 1-May-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  ->  ( -.  ( ph  ->  -.  ps )  <->  (
 ph  /\  ps )
 ) ) )
 
Theorempm4.67dc 817 Theorem *4.67 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 1-May-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  ->  ( -.  ( -.  ph  ->  -.  ps )  <->  ( -.  ph  /\  ps )
 ) ) )
 
Theoremannimim 818 Express conjunction in terms of implication. One direction of Theorem *4.61 of [WhiteheadRussell] p. 120. The converse holds for decidable propositions, as can be seen at annimdc 881. (Contributed by Jim Kingdon, 24-Dec-2017.)
 |-  ( ( ph  /\  -.  ps )  ->  -.  ( ph  ->  ps ) )
 
Theorempm4.65r 819 One direction of Theorem *4.65 of [WhiteheadRussell] p. 120. The converse holds in classical logic. (Contributed by Jim Kingdon, 28-Jul-2018.)
 |-  ( ( -.  ph  /\ 
 -.  ps )  ->  -.  ( -.  ph  ->  ps )
 )
 
Theoremdcim 820 An implication between two decidable propositions is decidable. (Contributed by Jim Kingdon, 28-Mar-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  -> DECID 
 ( ph  ->  ps )
 ) )
 
Theoremimanim 821 Express implication in terms of conjunction. The converse only holds given a decidability condition; see imandc 822. (Contributed by Jim Kingdon, 24-Dec-2017.)
 |-  ( ( ph  ->  ps )  ->  -.  ( ph  /\  -.  ps )
 )
 
Theoremimandc 822 Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176, with an added decidability condition. The forward direction, imanim 821, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 25-Apr-2018.)
 |-  (DECID 
 ps  ->  ( ( ph  ->  ps )  <->  -.  ( ph  /\  -.  ps ) ) )
 
Theorempm4.14dc 823 Theorem *4.14 of [WhiteheadRussell] p. 117, given a decidability condition. (Contributed by Jim Kingdon, 24-Apr-2018.)
 |-  (DECID 
 ch  ->  ( ( (
 ph  /\  ps )  ->  ch )  <->  ( ( ph  /\ 
 -.  ch )  ->  -.  ps ) ) )
 
Theorempm3.37 824 Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.)
 |-  ( ( ( ph  /\ 
 ps )  ->  ch )  ->  ( ( ph  /\  -.  ch )  ->  -.  ps )
 )
 
Theorempm4.15 825 Theorem *4.15 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
 |-  ( ( ( ph  /\ 
 ps )  ->  -.  ch ) 
 <->  ( ( ps  /\  ch )  ->  -.  ph )
 )
 
Theorempm2.54dc 826 Deriving disjunction from implication for a decidable proposition. Based on theorem *2.54 of [WhiteheadRussell] p. 107. The converse, pm2.53 674, holds whether the proposition is decidable or not. (Contributed by Jim Kingdon, 26-Mar-2018.)
 |-  (DECID 
 ph  ->  ( ( -.  ph  ->  ps )  ->  ( ph  \/  ps ) ) )
 
Theoremdfordc 827 Definition of 'or' in terms of negation and implication for a decidable proposition. Based on definition of [Margaris] p. 49. One direction, pm2.53 674, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 26-Mar-2018.)
 |-  (DECID 
 ph  ->  ( ( ph  \/  ps )  <->  ( -.  ph  ->  ps ) ) )
 
Theorempm2.25dc 828 Elimination of disjunction based on a disjunction, for a decidable proposition. Based on theorem *2.25 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
 |-  (DECID 
 ph  ->  ( ph  \/  ( ( ph  \/  ps )  ->  ps )
 ) )
 
Theorempm2.68dc 829 Concluding disjunction from implication for a decidable proposition. Based on theorem *2.68 of [WhiteheadRussell] p. 108. Converse of pm2.62 700 and one half of dfor2dc 830. (Contributed by Jim Kingdon, 27-Mar-2018.)
 |-  (DECID 
 ph  ->  ( ( (
 ph  ->  ps )  ->  ps )  ->  ( ph  \/  ps ) ) )
 
Theoremdfor2dc 830 Logical 'or' expressed in terms of implication only, for a decidable proposition. Based on theorem *5.25 of [WhiteheadRussell] p. 124. (Contributed by Jim Kingdon, 27-Mar-2018.)
 |-  (DECID 
 ph  ->  ( ( ph  \/  ps )  <->  ( ( ph  ->  ps )  ->  ps )
 ) )
 
Theoremimimorbdc 831 Simplify an implication between implications, for a decidable proposition. (Contributed by Jim Kingdon, 18-Mar-2018.)
 |-  (DECID 
 ps  ->  ( ( ( ps  ->  ch )  ->  ( ph  ->  ch )
 ) 
 <->  ( ph  ->  ( ps  \/  ch ) ) ) )
 
Theoremimordc 832 Implication in terms of disjunction for a decidable proposition. Based on theorem *4.6 of [WhiteheadRussell] p. 120. The reverse direction, imorr 833, holds for all propositions. (Contributed by Jim Kingdon, 20-Apr-2018.)
 |-  (DECID 
 ph  ->  ( ( ph  ->  ps )  <->  ( -.  ph  \/  ps ) ) )
 
Theoremimorr 833 Implication in terms of disjunction. One direction of theorem *4.6 of [WhiteheadRussell] p. 120. The converse holds for decidable propositions, as seen at imordc 832. (Contributed by Jim Kingdon, 21-Jul-2018.)
 |-  ( ( -.  ph  \/  ps )  ->  ( ph  ->  ps ) )
 
Theorempm4.62dc 834 Implication in terms of disjunction. Like Theorem *4.62 of [WhiteheadRussell] p. 120, but for a decidable antecedent. (Contributed by Jim Kingdon, 21-Apr-2018.)
 |-  (DECID 
 ph  ->  ( ( ph  ->  -.  ps )  <->  ( -.  ph  \/  -.  ps ) ) )
 
Theoremianordc 835 Negated conjunction in terms of disjunction (DeMorgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120, but where one proposition is decidable. The reverse direction, pm3.14 703, holds for all propositions, but the equivalence only holds where one proposition is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.)
 |-  (DECID 
 ph  ->  ( -.  ( ph  /\  ps )  <->  ( -.  ph  \/  -.  ps ) ) )
 
Theoremoibabs 836 Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)
 |-  ( ( ( ph  \/  ps )  ->  ( ph 
 <->  ps ) )  <->  ( ph  <->  ps ) )
 
Theorempm4.64dc 837 Theorem *4.64 of [WhiteheadRussell] p. 120, given a decidability condition. The reverse direction, pm2.53 674, holds for all propositions. (Contributed by Jim Kingdon, 2-May-2018.)
 |-  (DECID 
 ph  ->  ( ( -.  ph  ->  ps )  <->  ( ph  \/  ps ) ) )
 
Theorempm4.66dc 838 Theorem *4.66 of [WhiteheadRussell] p. 120, given a decidability condition. (Contributed by Jim Kingdon, 2-May-2018.)
 |-  (DECID 
 ph  ->  ( ( -.  ph  ->  -.  ps )  <->  (
 ph  \/  -.  ps )
 ) )
 
Theorempm4.52im 839 One direction of theorem *4.52 of [WhiteheadRussell] p. 120. The converse also holds in classical logic. (Contributed by Jim Kingdon, 27-Jul-2018.)
 |-  ( ( ph  /\  -.  ps )  ->  -.  ( -.  ph  \/  ps )
 )
 
Theorempm4.53r 840 One direction of theorem *4.53 of [WhiteheadRussell] p. 120. The converse also holds in classical logic. (Contributed by Jim Kingdon, 27-Jul-2018.)
 |-  ( ( -.  ph  \/  ps )  ->  -.  ( ph  /\  -.  ps )
 )
 
Theorempm4.54dc 841 Theorem *4.54 of [WhiteheadRussell] p. 120, for decidable propositions. One form of DeMorgan's law. (Contributed by Jim Kingdon, 2-May-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  ->  ( ( -.  ph  /\  ps )  <->  -.  ( ph  \/  -. 
 ps ) ) ) )
 
Theorempm4.56 842 Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
 |-  ( ( -.  ph  /\ 
 -.  ps )  <->  -.  ( ph  \/  ps ) )
 
Theoremoranim 843 Disjunction in terms of conjunction (DeMorgan's law). One direction of Theorem *4.57 of [WhiteheadRussell] p. 120. The converse does not hold intuitionistically but does hold in classical logic. (Contributed by Jim Kingdon, 25-Jul-2018.)
 |-  ( ( ph  \/  ps )  ->  -.  ( -.  ph  /\  -.  ps ) )
 
Theorempm4.78i 844 Implication distributes over disjunction. One direction of Theorem *4.78 of [WhiteheadRussell] p. 121. The converse holds in classical logic. (Contributed by Jim Kingdon, 15-Jan-2018.)
 |-  ( ( ( ph  ->  ps )  \/  ( ph  ->  ch ) )  ->  ( ph  ->  ( ps  \/  ch ) ) )
 
Theorempm4.79dc 845 Equivalence between a disjunction of two implications, and a conjunction and an implication. Based on theorem *4.79 of [WhiteheadRussell] p. 121 but with additional decidability antecedents. (Contributed by Jim Kingdon, 28-Mar-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  ->  ( ( ( ps  ->  ph )  \/  ( ch  ->  ph )
 ) 
 <->  ( ( ps  /\  ch )  ->  ph ) ) ) )
 
Theorempm5.17dc 846 Two ways of stating exclusive-or which are equivalent for a decidable proposition. Based on theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by Jim Kingdon, 16-Apr-2018.)
 |-  (DECID 
 ps  ->  ( ( (
 ph  \/  ps )  /\  -.  ( ph  /\  ps ) )  <->  ( ph  <->  -.  ps ) ) )
 
Theorempm2.85dc 847 Reverse distribution of disjunction over implication, given decidability. Based on theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by Jim Kingdon, 1-Apr-2018.)
 |-  (DECID 
 ph  ->  ( ( (
 ph  \/  ps )  ->  ( ph  \/  ch ) )  ->  ( ph  \/  ( ps  ->  ch )
 ) ) )
 
Theoremorimdidc 848 Disjunction distributes over implication. The forward direction, pm2.76 755, is valid intuitionistically. The reverse direction holds if  ph is decidable, as can be seen at pm2.85dc 847. (Contributed by Jim Kingdon, 1-Apr-2018.)
 |-  (DECID 
 ph  ->  ( ( ph  \/  ( ps  ->  ch )
 ) 
 <->  ( ( ph  \/  ps )  ->  ( ph  \/  ch ) ) ) )
 
Theorempm2.26dc 849 Decidable proposition version of theorem *2.26 of [WhiteheadRussell] p. 104. (Contributed by Jim Kingdon, 20-Apr-2018.)
 |-  (DECID 
 ph  ->  ( -.  ph  \/  ( ( ph  ->  ps )  ->  ps )
 ) )
 
Theorempm4.81dc 850 Theorem *4.81 of [WhiteheadRussell] p. 122, for decidable propositions. This one needs a decidability condition, but compare with pm4.8 656 which holds for all propositions. (Contributed by Jim Kingdon, 4-Jul-2018.)
 |-  (DECID 
 ph  ->  ( ( -.  ph  ->  ph )  <->  ph ) )
 
Theorempm5.11dc 851 A decidable proposition or its negation implies a second proposition. Based on theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 29-Mar-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  ->  ( ( ph  ->  ps )  \/  ( -.  ph  ->  ps )
 ) ) )
 
Theorempm5.12dc 852 Excluded middle with antecedents for a decidable consequent. Based on theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 30-Mar-2018.)
 |-  (DECID 
 ps  ->  ( ( ph  ->  ps )  \/  ( ph  ->  -.  ps )
 ) )
 
Theorempm5.14dc 853 A decidable proposition is implied by or implies other propositions. Based on theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 30-Mar-2018.)
 |-  (DECID 
 ps  ->  ( ( ph  ->  ps )  \/  ( ps  ->  ch ) ) )
 
Theorempm5.13dc 854 An implication holds in at least one direction, where one proposition is decidable. Based on theorem *5.13 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 30-Mar-2018.)
 |-  (DECID 
 ps  ->  ( ( ph  ->  ps )  \/  ( ps  ->  ph ) ) )
 
Theorempm5.55dc 855 A disjunction is equivalent to one of its disjuncts, given a decidable disjunct. Based on theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by Jim Kingdon, 30-Mar-2018.)
 |-  (DECID 
 ph  ->  ( ( (
 ph  \/  ps )  <->  ph )  \/  ( (
 ph  \/  ps )  <->  ps ) ) )
 
Theorempeircedc 856 Peirce's theorem for a decidable proposition. This odd-looking theorem can be seen as an alternative to exmiddc 780, condc 785, or notnotrdc 787 in the sense of expressing the "difference" between an intuitionistic system of propositional calculus and a classical system. In intuitionistic logic, it only holds for decidable propositions. (Contributed by Jim Kingdon, 3-Jul-2018.)
 |-  (DECID 
 ph  ->  ( ( (
 ph  ->  ps )  ->  ph )  -> 
 ph ) )
 
Theoremlooinvdc 857 The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz, but where one of the propositions is decidable. Using dfor2dc 830, we can see that this expresses "disjunction commutes." Theorem *2.69 of [WhiteheadRussell] p. 108 (plus the decidability condition). (Contributed by NM, 12-Aug-2004.)
 |-  (DECID 
 ph  ->  ( ( (
 ph  ->  ps )  ->  ps )  ->  ( ( ps  ->  ph )  ->  ph ) ) )
 
1.2.10  Testable propositions
 
Theoremdftest 858 A proposition is testable iff its negative or double-negative is true. See Chapter 2 [Moschovakis] p. 2.

Our notation for testability is DECID  -. before the formula in question. For example, DECID  -.  x  =  y corresponds to "x = y is testable". (Contributed by David A. Wheeler, 13-Aug-2018.)

 |-  (DECID 
 -.  ph  <->  ( -.  ph  \/  -.  -.  ph )
 )
 
Theoremtestbitestn 859 A proposition is testable iff its negation is testable. See also dcn 782 (which could be read as "Decidability implies testability"). (Contributed by David A. Wheeler, 6-Dec-2018.)
 |-  (DECID 
 -.  ph  <-> DECID  -.  -.  ph )
 
Theoremstabtestimpdc 860 "Stable and testable" is equivalent to decidable. (Contributed by David A. Wheeler, 13-Aug-2018.)
 |-  ( (STAB 
 ph  /\ DECID  -.  ph )  <-> DECID  ph )
 
1.2.11  Miscellaneous theorems of propositional calculus
 
Theorempm5.21nd 861 Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.)
 |-  ( ( ph  /\  ps )  ->  th )   &    |-  ( ( ph  /\ 
 ch )  ->  th )   &    |-  ( th  ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  ( ps  <->  ch ) )
 
Theorempm5.35 862 Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
 |-  ( ( ( ph  ->  ps )  /\  ( ph  ->  ch ) )  ->  ( ph  ->  ( ps  <->  ch ) ) )
 
Theorempm5.54dc 863 A conjunction is equivalent to one of its conjuncts, given a decidable conjunct. Based on theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by Jim Kingdon, 30-Mar-2018.)
 |-  (DECID 
 ph  ->  ( ( (
 ph  /\  ps )  <->  ph )  \/  ( (
 ph  /\  ps )  <->  ps ) ) )
 
Theorembaib 864 Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
 |-  ( ph  <->  ( ps  /\  ch ) )   =>    |-  ( ps  ->  ( ph 
 <->  ch ) )
 
Theorembaibr 865 Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
 |-  ( ph  <->  ( ps  /\  ch ) )   =>    |-  ( ps  ->  ( ch 
 <-> 
 ph ) )
 
Theoremrbaib 866 Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
 |-  ( ph  <->  ( ps  /\  ch ) )   =>    |-  ( ch  ->  ( ph 
 <->  ps ) )
 
Theoremrbaibr 867 Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
 |-  ( ph  <->  ( ps  /\  ch ) )   =>    |-  ( ch  ->  ( ps 
 <-> 
 ph ) )
 
Theorembaibd 868 Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
 |-  ( ph  ->  ( ps 
 <->  ( ch  /\  th ) ) )   =>    |-  ( ( ph  /\ 
 ch )  ->  ( ps 
 <-> 
 th ) )
 
Theoremrbaibd 869 Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
 |-  ( ph  ->  ( ps 
 <->  ( ch  /\  th ) ) )   =>    |-  ( ( ph  /\ 
 th )  ->  ( ps 
 <->  ch ) )
 
Theorempm5.44 870 Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
 |-  ( ( ph  ->  ps )  ->  ( ( ph  ->  ch )  <->  ( ph  ->  ( ps  /\  ch )
 ) ) )
 
Theorempm5.6dc 871 Conjunction in antecedent versus disjunction in consequent, for a decidable proposition. Theorem *5.6 of [WhiteheadRussell] p. 125, with decidability condition added. The reverse implication holds for all propositions (see pm5.6r 872). (Contributed by Jim Kingdon, 2-Apr-2018.)
 |-  (DECID 
 ps  ->  ( ( (
 ph  /\  -.  ps )  ->  ch )  <->  ( ph  ->  ( ps  \/  ch )
 ) ) )
 
Theorempm5.6r 872 Conjunction in antecedent versus disjunction in consequent. One direction of Theorem *5.6 of [WhiteheadRussell] p. 125. If  ps is decidable, the converse also holds (see pm5.6dc 871). (Contributed by Jim Kingdon, 4-Aug-2018.)
 |-  ( ( ph  ->  ( ps  \/  ch )
 )  ->  ( ( ph  /\  -.  ps )  ->  ch ) )
 
Theoremorcanai 873 Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
 |-  ( ph  ->  ( ps  \/  ch ) )   =>    |-  ( ( ph  /\  -.  ps )  ->  ch )
 
Theoremintnan 874 Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
 |- 
 -.  ph   =>    |- 
 -.  ( ps  /\  ph )
 
Theoremintnanr 875 Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
 |- 
 -.  ph   =>    |- 
 -.  ( ph  /\  ps )
 
Theoremintnand 876 Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
 |-  ( ph  ->  -.  ps )   =>    |-  ( ph  ->  -.  ( ch  /\  ps ) )
 
Theoremintnanrd 877 Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
 |-  ( ph  ->  -.  ps )   =>    |-  ( ph  ->  -.  ( ps  /\  ch ) )
 
Theoremdcan 878 A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  -> DECID 
 ( ph  /\  ps )
 ) )
 
Theoremdcor 879 A disjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  -> DECID 
 ( ph  \/  ps )
 ) )
 
Theoremdcbi 880 An equivalence of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  -> DECID 
 ( ph  <->  ps ) ) )
 
Theoremannimdc 881 Express conjunction in terms of implication. The forward direction, annimim 818, is valid for all propositions, but as an equivalence, it requires a decidability condition. (Contributed by Jim Kingdon, 25-Apr-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  ->  ( ( ph  /\ 
 -.  ps )  <->  -.  ( ph  ->  ps ) ) ) )
 
Theorempm4.55dc 882 Theorem *4.55 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 2-May-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  ->  ( -.  ( -.  ph  /\  ps )  <->  (
 ph  \/  -.  ps )
 ) ) )
 
Theoremorandc 883 Disjunction in terms of conjunction (De Morgan's law), for decidable propositions. Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by Jim Kingdon, 13-Dec-2021.)
 |-  ( (DECID 
 ph  /\ DECID  ps )  ->  (
 ( ph  \/  ps )  <->  -.  ( -.  ph  /\  -.  ps ) ) )
 
Theoremmpbiran 884 Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) (Revised by NM, 9-Jan-2015.)
 |- 
 ps   &    |-  ( ph  <->  ( ps  /\  ch ) )   =>    |-  ( ph  <->  ch )
 
Theoremmpbiran2 885 Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.)
 |- 
 ch   &    |-  ( ph  <->  ( ps  /\  ch ) )   =>    |-  ( ph  <->  ps )
 
Theoremmpbir2an 886 Detach a conjunction of truths in a biconditional. (Contributed by NM, 10-May-2005.) (Revised by NM, 9-Jan-2015.)
 |- 
 ps   &    |- 
 ch   &    |-  ( ph  <->  ( ps  /\  ch ) )   =>    |-  ph
 
Theoremmpbi2and 887 Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
 |-  ( ph  ->  ps )   &    |-  ( ph  ->  ch )   &    |-  ( ph  ->  ( ( ps  /\  ch ) 
 <-> 
 th ) )   =>    |-  ( ph  ->  th )
 
Theoremmpbir2and 888 Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
 |-  ( ph  ->  ch )   &    |-  ( ph  ->  th )   &    |-  ( ph  ->  ( ps  <->  ( ch  /\  th ) ) )   =>    |-  ( ph  ->  ps )
 
Theorempm5.62dc 889 Theorem *5.62 of [WhiteheadRussell] p. 125, for a decidable proposition. (Contributed by Jim Kingdon, 12-May-2018.)
 |-  (DECID 
 ps  ->  ( ( (
 ph  /\  ps )  \/  -.  ps )  <->  ( ph  \/  -. 
 ps ) ) )
 
Theorempm5.63dc 890 Theorem *5.63 of [WhiteheadRussell] p. 125, for a decidable proposition. (Contributed by Jim Kingdon, 12-May-2018.)
 |-  (DECID 
 ph  ->  ( ( ph  \/  ps )  <->  ( ph  \/  ( -.  ph  /\  ps )
 ) ) )
 
Theorembianfi 891 A wff conjoined with falsehood is false. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
 |- 
 -.  ph   =>    |-  ( ph  <->  ( ps  /\  ph ) )
 
Theorembianfd 892 A wff conjoined with falsehood is false. (Contributed by NM, 27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.)
 |-  ( ph  ->  -.  ps )   =>    |-  ( ph  ->  ( ps 
 <->  ( ps  /\  ch ) ) )
 
Theorempm4.43 893 Theorem *4.43 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
 |-  ( ph  <->  ( ( ph  \/  ps )  /\  ( ph  \/  -.  ps )
 ) )
 
Theorempm4.82 894 Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
 |-  ( ( ( ph  ->  ps )  /\  ( ph  ->  -.  ps )
 ) 
 <->  -.  ph )
 
Theorempm4.83dc 895 Theorem *4.83 of [WhiteheadRussell] p. 122, for decidable propositions. As with other case elimination theorems, like pm2.61dc 798, it only holds for decidable propositions. (Contributed by Jim Kingdon, 12-May-2018.)
 |-  (DECID 
 ph  ->  ( ( (
 ph  ->  ps )  /\  ( -.  ph  ->  ps )
 ) 
 <->  ps ) )
 
Theorembiantr 896 A transitive law of equivalence. Compare Theorem *4.22 of [WhiteheadRussell] p. 117. (Contributed by NM, 18-Aug-1993.)
 |-  ( ( ( ph  <->  ps )  /\  ( ch  <->  ps ) )  ->  ( ph  <->  ch ) )
 
Theoremorbididc 897 Disjunction distributes over the biconditional, for a decidable proposition. Based on an axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.3384. (Contributed by Jim Kingdon, 2-Apr-2018.)
 |-  (DECID 
 ph  ->  ( ( ph  \/  ( ps  <->  ch ) )  <->  ( ( ph  \/  ps )  <->  ( ph  \/  ch ) ) ) )
 
Theorempm5.7dc 898 Disjunction distributes over the biconditional, for a decidable proposition. Based on theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbididc 897. (Contributed by Jim Kingdon, 2-Apr-2018.)
 |-  (DECID 
 ch  ->  ( ( (
 ph  \/  ch )  <->  ( ps  \/  ch )
 ) 
 <->  ( ch  \/  ( ph 
 <->  ps ) ) ) )
 
Theorembigolden 899 Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
 |-  ( ( ( ph  /\ 
 ps )  <->  ph )  <->  ( ps  <->  ( ph  \/  ps ) ) )
 
Theoremanordc 900 Conjunction in terms of disjunction (DeMorgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120, but where the propositions are decidable. The forward direction, pm3.1 704, holds for all propositions, but the equivalence only holds given decidability. (Contributed by Jim Kingdon, 21-Apr-2018.)
 |-  (DECID 
 ph  ->  (DECID 
 ps  ->  ( ( ph  /\ 
 ps )  <->  -.  ( -.  ph  \/  -.  ps ) ) ) )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800801-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-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11363
  Copyright terms: Public domain < Previous  Next >