Home | Metamath
Proof Explorer Theorem List (p. 11 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dedlem0b 1001 | Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994.) |
Theorem | dedlema 1002 | Lemma for weak deduction theorem. See also ifptru 1023. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Theorem | dedlemb 1003 | Lemma for weak deduction theorem. See also ifpfal 1024. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Theorem | pm4.42 1004 | Theorem *4.42 of [WhiteheadRussell] p. 119. See also ifpid 1025. (Contributed by Roy F. Longton, 21-Jun-2005.) |
Theorem | prlem1 1005 | A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 5-Jan-2013.) |
Theorem | prlem2 1006 | A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 21-Jun-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 9-Dec-2012.) |
Theorem | oplem1 1007 | A specialized lemma for set theory (ordered pair theorem). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Wolf Lammen, 8-Dec-2012.) |
Theorem | dn1 1008 | A single axiom for Boolean algebra known as DN1. See McCune, Veroff, Fitelson, Harris, Feist, Wos, Short single axioms for Boolean algebra, Journal of Automated Reasoning, 29(1):1--16, 2002. (https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf). (Contributed by Jeff Hankins, 3-Jul-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 6-Jan-2013.) |
Theorem | bianir 1009 | A closed form of mpbir 221, analogous to pm2.27 42 (assertion). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Roger Witte, 17-Aug-2020.) |
Theorem | jaoi2 1010 | Inference removing a negated conjunct in a disjunction of an antecedent if this conjunct is part of the disjunction. (Contributed by Alexander van der Vekens, 3-Nov-2017.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) |
Theorem | jaoi3 1011 | Inference separating a disjunct of an antecedent. (Contributed by Alexander van der Vekens, 25-May-2018.) |
This subsection introduces the conditional operator for propositions, denoted by if- (see df-ifp 1013). It is the analogue for propositions of the conditional operator for classes (see df-if 4087). | ||
Syntax | wif 1012 | Extend class notation to include the conditional operator for propositions. |
if- | ||
Definition | df-ifp 1013 |
Definition of the conditional operator for propositions. The value of
if-
is if is true and if
false. See dfifp2 1014, dfifp3 1015, dfifp4 1016, dfifp5 1017, dfifp6 1018 and
dfifp7 1019 for alternate definitions.
This definition (in the form of dfifp2 1014) appears in Section II.24 of [Church] p. 129 (Definition D12 page 132), where it is called "conditioned disjunction". Church's corresponds to our if- (note the permutation of the first two variables). Church uses the conditional operator as an intermediate step to prove completeness of some systems of connectives. The first result is that the system if- is complete: for the induction step, consider a wff with n+1 variables; single out one variable, say ; when one sets to True (resp. False), then what remains is a wff of n variables, so by the induction hypothesis it corresponds to a formula using only if- , say (resp. ); therefore, the formula if- represents the initial wff. Now, since and similar systems suffice to express if- , they are also complete. (Contributed by BJ, 22-Jun-2019.) |
if- | ||
Theorem | dfifp2 1014 | Alternate definition of the conditional operator for propositions. The value of if- is "if then , and if not then ." This is the definition used in Section II.24 of [Church] p. 129 (Definition D12 page 132) (see comment of df-ifp 1013). (Contributed by BJ, 22-Jun-2019.) |
if- | ||
Theorem | dfifp3 1015 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.) |
if- | ||
Theorem | dfifp4 1016 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.) |
if- | ||
Theorem | dfifp5 1017 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.) |
if- | ||
Theorem | dfifp6 1018 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.) |
if- | ||
Theorem | dfifp7 1019 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.) |
if- | ||
Theorem | anifp 1020 | The conditional operator is implied by the conjunction of its possible outputs. Dual statement of ifpor 1021. (Contributed by BJ, 30-Sep-2019.) |
if- | ||
Theorem | ifpor 1021 | The conditional operator implies the disjunction of its possible outputs. Dual statement of anifp 1020. (Contributed by BJ, 1-Oct-2019.) |
if- | ||
Theorem | ifpn 1022 | Conditional operator for the negation of a proposition. (Contributed by BJ, 30-Sep-2019.) |
if- if- | ||
Theorem | ifptru 1023 | Value of the conditional operator for propositions when its first argument is true. Analogue for propositions of iftrue 4092. This is essentially dedlema 1002. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 10-Jul-2020.) |
if- | ||
Theorem | ifpfal 1024 | Value of the conditional operator for propositions when its first argument is false. Analogue for propositions of iffalse 4095. This is essentially dedlemb 1003. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 25-Jun-2020.) |
if- | ||
Theorem | ifpid 1025 | Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of ifid 4125. This is essentially pm4.42 1004. (Contributed by BJ, 20-Sep-2019.) |
if- | ||
Theorem | casesifp 1026 | Version of cases 992 expressed using if-. Case disjunction according to the value of . One can see this as a proof that the two hypotheses characterize the conditional operator for propositions. For the converses, see ifptru 1023 and ifpfal 1024. (Contributed by BJ, 20-Sep-2019.) |
if- | ||
Theorem | ifpbi123d 1027 | Equality deduction for conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) |
if- if- | ||
Theorem | ifpimpda 1028 | Separation of the values of the conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 27-Feb-2021.) |
if- | ||
Theorem | 1fpid3 1029 | The value of the conditional operator for propositions is its third argument if the first and second argument imply the third argument. (Contributed by AV, 4-Apr-2021.) |
if- | ||
This subsection contains a few results related to the weak deduction theorem. For more information, see the Weak Deduction Theorem page mmdeduction.html. | ||
Theorem | elimh 1030 | Hypothesis builder for the weak deduction theorem. For more information, see the Weak Deduction Theorem page mmdeduction.html. (Contributed by NM, 26-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) |
if- if- | ||
Theorem | dedt 1031 | The weak deduction theorem. For more information, see the Weak Deduction Theorem page mmdeduction.html. (Contributed by NM, 26-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) |
if- | ||
Theorem | con3ALT 1032 | Proof of con3 149 from its associated inference con3i 150 that illustrates the use of the weak deduction theorem dedt 1031. (Contributed by NM, 27-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | elimhOLD 1033 | Old version of elimh 1030. Obsolete as of 16-Mar-2021. (Contributed by NM, 26-Jun-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | dedtOLD 1034 | Old version of dedt 1031. Obsolete as of 16-Mar-2021. (Contributed by NM, 26-Jun-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | con3OLD 1035 | Old version of con3ALT 1032. Obsolete as of 16-Mar-2021. (Contributed by NM, 27-Jun-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
Syntax | w3o 1036 | Extend wff definition to include three-way disjunction ('or'). |
Syntax | w3a 1037 | Extend wff definition to include three-way conjunction ('and'). |
Definition | df-3or 1038 | Define disjunction ('or') of three wff's. Definition *2.33 of [WhiteheadRussell] p. 105. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law orass 546. (Contributed by NM, 8-Apr-1994.) |
Definition | df-3an 1039 | Define conjunction ('and') of three wff's. Definition *4.34 of [WhiteheadRussell] p. 118. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law anass 681. (Contributed by NM, 8-Apr-1994.) |
Theorem | 3orass 1040 | Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.) |
Theorem | 3orel1 1041 | Partial elimination of a triple disjunction by denial of a disjunct. (Contributed by Scott Fenton, 26-Mar-2011.) |
Theorem | 3anass 1042 | Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.) |
Theorem | 3anrot 1043 | Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.) |
Theorem | 3orrot 1044 | Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.) |
Theorem | 3ancoma 1045 | Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Theorem | 3orcoma 1046 | Commutation law for triple disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.) |
Theorem | 3ancomb 1047 | Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Theorem | 3orcomb 1048 | Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.) |
Theorem | 3anrev 1049 | Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Theorem | 3anan32 1050 | Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | 3anan12 1051 | Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | anandi3 1052 | Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.) |
Theorem | anandi3r 1053 | Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.) |
Theorem | 3anor 1054 | Triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) |
Theorem | 3ianor 1055 | Negated triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | 3ioran 1056 | Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.) |
Theorem | 3oran 1057 | Triple disjunction in terms of triple conjunction. (Contributed by NM, 8-Oct-2012.) |
Theorem | 3simpa 1058 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Theorem | 3simpb 1059 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Theorem | 3simpc 1060 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | simp1 1061 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Theorem | simp2 1062 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Theorem | simp3 1063 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
Theorem | simpl1 1064 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Theorem | simpl2 1065 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Theorem | simpl3 1066 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Theorem | simpr1 1067 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Theorem | simpr2 1068 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Theorem | simpr3 1069 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Theorem | simp1i 1070 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
Theorem | simp2i 1071 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
Theorem | simp3i 1072 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
Theorem | simp1d 1073 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
Theorem | simp2d 1074 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
Theorem | simp3d 1075 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
Theorem | simp1bi 1076 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | simp2bi 1077 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | simp3bi 1078 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Theorem | 3adant1 1079 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
Theorem | 3adant2 1080 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
Theorem | 3adant3 1081 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
Theorem | 3ad2ant1 1082 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
Theorem | 3ad2ant2 1083 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
Theorem | 3ad2ant3 1084 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
Theorem | simp1l 1085 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Theorem | simp1r 1086 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Theorem | simp2l 1087 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Theorem | simp2r 1088 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Theorem | simp3l 1089 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Theorem | simp3r 1090 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
Theorem | simp11 1091 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
Theorem | simp12 1092 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
Theorem | simp13 1093 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
Theorem | simp21 1094 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
Theorem | simp22 1095 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
Theorem | simp23 1096 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
Theorem | simp31 1097 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
Theorem | simp32 1098 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
Theorem | simp33 1099 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
Theorem | simpll1 1100 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |