P. 10 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 901-1000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	imandc 901	Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176, with an added decidability condition. The forward direction, imanim 699, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 25-Apr-2018.)
|- (DECID ps -> ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) ) )
Theorem	pm4.14dc 902	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 ) ) )
Theorem	pm2.54dc 903	Deriving disjunction from implication for a decidable proposition. Based on theorem *2.54 of [WhiteheadRussell] p. 107. The converse, pm2.53 734, holds whether the proposition is decidable or not. (Contributed by Jim Kingdon, 26-Mar-2018.)
|- (DECID ph -> ( ( -. ph -> ps ) -> ( ph \/ ps ) ) )
Theorem	dfordc 904	Definition of disjunction in terms of negation and implication for a decidable proposition. Based on definition of [Margaris] p. 49. One direction, pm2.53 734, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 26-Mar-2018.)
|- (DECID ph -> ( ( ph \/ ps ) <-> ( -. ph -> ps ) ) )
Theorem	pm2.25dc 905	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 ) ) )
Theorem	pm2.68dc 906	Concluding disjunction from implication for a decidable proposition. Based on theorem *2.68 of [WhiteheadRussell] p. 108. Converse of pm2.62 760 and one half of dfor2dc 907. (Contributed by Jim Kingdon, 27-Mar-2018.)
|- (DECID ph -> ( ( ( ph -> ps ) -> ps ) -> ( ph \/ ps ) ) )
Theorem	dfor2dc 907	Disjunction 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 ) ) )
Theorem	imimorbdc 908	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 ) ) ) )
Theorem	imordc 909	Implication in terms of disjunction for a decidable proposition. Based on theorem *4.6 of [WhiteheadRussell] p. 120. The reverse direction, imorr 733, holds for all propositions. (Contributed by Jim Kingdon, 20-Apr-2018.)
|- (DECID ph -> ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) )
Theorem	pm4.62dc 910	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 ) ) )
Theorem	ianordc 911	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 765, 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 ) ) )
Theorem	pm4.64dc 912	Theorem *4.64 of [WhiteheadRussell] p. 120, given a decidability condition. The reverse direction, pm2.53 734, holds for all propositions. (Contributed by Jim Kingdon, 2-May-2018.)
|- (DECID ph -> ( ( -. ph -> ps ) <-> ( ph \/ ps ) ) )
Theorem	pm4.66dc 913	Theorem *4.66 of [WhiteheadRussell] p. 120, given a decidability condition. (Contributed by Jim Kingdon, 2-May-2018.)
|- (DECID ph -> ( ( -. ph -> -. ps ) <-> ( ph \/ -. ps ) ) )
Theorem	pm4.54dc 914	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 ) ) ) )
Theorem	pm4.79dc 915	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 ) ) ) )
Theorem	pm5.17dc 916	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 ) ) )
Theorem	pm2.85dc 917	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 ) ) ) )
Theorem	orimdidc 918	Disjunction distributes over implication. The forward direction, pm2.76 820, is valid intuitionistically. The reverse direction holds if ph is decidable, as can be seen at pm2.85dc 917. (Contributed by Jim Kingdon, 1-Apr-2018.)
|- (DECID ph -> ( ( ph \/ ( ps -> ch ) ) <-> ( ( ph \/ ps ) -> ( ph \/ ch ) ) ) )
Theorem	pm2.26dc 919	Decidable proposition version of theorem *2.26 of [WhiteheadRussell] p. 104. (Contributed by Jim Kingdon, 20-Apr-2018.)
|- (DECID ph -> ( -. ph \/ ( ( ph -> ps ) -> ps ) ) )
Theorem	pm4.81dc 920	Theorem *4.81 of [WhiteheadRussell] p. 122, for decidable propositions. This one needs a decidability condition, but compare with pm4.8 719 which holds for all propositions. (Contributed by Jim Kingdon, 4-Jul-2018.)
|- (DECID ph -> ( ( -. ph -> ph ) <-> ph ) )
Theorem	pm5.11dc 921	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 ) ) ) )
Theorem	pm5.12dc 922	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 ) ) )
Theorem	pm5.14dc 923	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 ) ) )
Theorem	pm5.13dc 924	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 ) ) )
Theorem	pm5.55dc 925	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 ) ) )
Theorem	peircedc 926	Peirce's theorem for a decidable proposition. This odd-looking theorem can be seen as an alternative to exmiddc 848, condc 865, or notnotrdc 855 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 ) )
Theorem	looinvdc 927	The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz, but where one of the propositions is decidable. Using dfor2dc 907, we can see that this expresses "disjunction is commutative". 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  Miscellaneous theorems of propositional calculus
Theorem	pm5.21nd 928	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 ) )
Theorem	pm5.35 929	Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) -> ( ph -> ( ps <-> ch ) ) )
Theorem	pm5.54dc 930	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 ) ) )
Theorem	baib 931	Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ph <-> ch ) )
Theorem	baibr 932	Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ch <-> ph ) )
Theorem	rbaib 933	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ch -> ( ph <-> ps ) )
Theorem	rbaibr 934	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ch -> ( ps <-> ph ) )
Theorem	baibd 935	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ ch ) -> ( ps <-> th ) )
Theorem	rbaibd 936	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ th ) -> ( ps <-> ch ) )
Theorem	pm5.44 937	Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) -> ( ( ph -> ch ) <-> ( ph -> ( ps /\ ch ) ) ) )
Theorem	pm5.6dc 938	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 939). (Contributed by Jim Kingdon, 2-Apr-2018.)
|- (DECID ps -> ( ( ( ph /\ -. ps ) -> ch ) <-> ( ph -> ( ps \/ ch ) ) ) )
Theorem	pm5.6r 939	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 938). (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( ph -> ( ps \/ ch ) ) -> ( ( ph /\ -. ps ) -> ch ) )
Theorem	orcanai 940	Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
|- ( ph -> ( ps \/ ch ) )   =>    |- ( ( ph /\ -. ps ) -> ch )
Theorem	intnan 941	Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
|- -. ph   =>    |- -. ( ps /\ ph )
Theorem	intnanr 942	Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
|- -. ph   =>    |- -. ( ph /\ ps )
Theorem	intnand 943	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. ( ch /\ ps ) )
Theorem	intnanrd 944	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. ( ps /\ ch ) )
Theorem	dcand 945	A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.) (Revised by BJ, 14-Nov-2024.)
|- ( ph -> DECID ps )   &    |- ( ph -> DECID ch )   =>    |- ( ph -> DECID ( ps /\ ch ) )
Theorem	dcan 946	A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
|- ( (DECID ph /\ DECID ps ) -> DECID ( ph /\ ps ) )
Theorem	dcan2 947	A conjunction of two decidable propositions is decidable, expressed in a curried form as compared to dcan 946. This is deprecated; it's trivial to recreate with ex 115, but it's here in case someone is using this older form. (Contributed by Jim Kingdon, 12-Apr-2018.) (New usage is discouraged.)
|- (DECID ph -> (DECID ps -> DECID ( ph /\ ps ) ) )
Theorem	dcor 948	A disjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.)
|- (DECID ph -> (DECID ps -> DECID ( ph \/ ps ) ) )
Theorem	dcbi 949	An equivalence of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
|- (DECID ph -> (DECID ps -> DECID ( ph <-> ps ) ) )
Theorem	annimdc 950	Express conjunction in terms of implication. The forward direction, annimim 697, 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 ) ) ) )
Theorem	pm4.55dc 951	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 ) ) ) )
Theorem	orandc 952	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 ) ) )
Theorem	mpbiran 953	Detach truth from conjunction in biconditional. (Contributed by NM, 27-Feb-1996.) (Revised by NM, 9-Jan-2015.)
|- ps   &    |- ( ph <-> ( ps /\ ch ) )   =>    |- ( ph <-> ch )
Theorem	mpbiran2 954	Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.) (Revised by NM, 9-Jan-2015.)
|- ch   &    |- ( ph <-> ( ps /\ ch ) )   =>    |- ( ph <-> ps )
Theorem	mpbir2an 955	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
Theorem	mpbi2and 956	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 )
Theorem	mpbir2and 957	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 )
Theorem	pm5.62dc 958	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 ) ) )
Theorem	pm5.63dc 959	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 ) ) ) )
Theorem	bianfi 960	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 ) )
Theorem	bianfd 961	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 ) ) )
Theorem	pm4.43 962	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 ) ) )
Theorem	pm4.82 963	Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> -. ps ) ) <-> -. ph )
Theorem	pm4.83dc 964	Theorem *4.83 of [WhiteheadRussell] p. 122, for decidable propositions. As with other case elimination theorems, like pm2.61dc 877, it only holds for decidable propositions. (Contributed by Jim Kingdon, 12-May-2018.)
|- (DECID ph -> ( ( ( ph -> ps ) /\ ( -. ph -> ps ) ) <-> ps ) )
Theorem	biantr 965	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 ) )
Theorem	orbididc 966	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 ) ) ) )
Theorem	pm5.7dc 967	Disjunction distributes over the biconditional, for a decidable proposition. Based on theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbididc 966. (Contributed by Jim Kingdon, 2-Apr-2018.)
|- (DECID ch -> ( ( ( ph \/ ch ) <-> ( ps \/ ch ) ) <-> ( ch \/ ( ph <-> ps ) ) ) )
Theorem	bigolden 968	Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
|- ( ( ( ph /\ ps ) <-> ph ) <-> ( ps <-> ( ph \/ ps ) ) )
Theorem	anordc 969	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 766, 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 ) ) ) )
Theorem	pm3.11dc 970	Theorem *3.11 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.1 766, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 22-Apr-2018.)
|- (DECID ph -> (DECID ps -> ( -. ( -. ph \/ -. ps ) -> ( ph /\ ps ) ) ) )
Theorem	pm3.12dc 971	Theorem *3.12 of [WhiteheadRussell] p. 111, but for decidable propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
|- (DECID ph -> (DECID ps -> ( ( -. ph \/ -. ps ) \/ ( ph /\ ps ) ) ) )
Theorem	pm3.13dc 972	Theorem *3.13 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.14 765, holds for all propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
|- (DECID ph -> (DECID ps -> ( -. ( ph /\ ps ) -> ( -. ph \/ -. ps ) ) ) )
Theorem	dn1dc 973	DN1 for decidable propositions. Without the decidability conditions, DN1 can serve as a single axiom for Boolean algebra. See http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf. (Contributed by Jim Kingdon, 22-Apr-2018.)
|- ( (DECID ph /\ (DECID ps /\ (DECID ch /\ DECID th ) ) ) -> ( -. ( -. ( -. ( ph \/ ps ) \/ ch ) \/ -. ( ph \/ -. ( -. ch \/ -. ( ch \/ th ) ) ) ) <-> ch ) )
Theorem	pm5.71dc 974	Decidable proposition version of theorem *5.71 of [WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.) (Modified for decidability by Jim Kingdon, 19-Apr-2018.)
|- (DECID ps -> ( ( ps -> -. ch ) -> ( ( ( ph \/ ps ) /\ ch ) <-> ( ph /\ ch ) ) ) )
Theorem	pm5.75 975	Theorem *5.75 of [WhiteheadRussell] p. 126. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2012.)
|- ( ( ( ch -> -. ps ) /\ ( ph <-> ( ps \/ ch ) ) ) -> ( ( ph /\ -. ps ) <-> ch ) )
Theorem	bimsc1 976	Removal of conjunct from one side of an equivalence. (Contributed by NM, 5-Aug-1993.)
|- ( ( ( ph -> ps ) /\ ( ch <-> ( ps /\ ph ) ) ) -> ( ch <-> ph ) )
Theorem	ccase 977	Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)
|- ( ( ph /\ ps ) -> ta )   &    |- ( ( ch /\ ps ) -> ta )   &    |- ( ( ph /\ th ) -> ta )   &    |- ( ( ch /\ th ) -> ta )   =>    |- ( ( ( ph \/ ch ) /\ ( ps \/ th ) ) -> ta )
Theorem	ccased 978	Deduction for combining cases. (Contributed by NM, 9-May-2004.)
|- ( ph -> ( ( ps /\ ch ) -> et ) )   &    |- ( ph -> ( ( th /\ ch ) -> et ) )   &    |- ( ph -> ( ( ps /\ ta ) -> et ) )   &    |- ( ph -> ( ( th /\ ta ) -> et ) )   =>    |- ( ph -> ( ( ( ps \/ th ) /\ ( ch \/ ta ) ) -> et ) )
Theorem	ccase2 979	Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
|- ( ( ph /\ ps ) -> ta )   &    |- ( ch -> ta )   &    |- ( th -> ta )   =>    |- ( ( ( ph \/ ch ) /\ ( ps \/ th ) ) -> ta )
Theorem	niabn 980	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
|- ph   =>    |- ( -. ps -> ( ( ch /\ ps ) <-> -. ph ) )
Theorem	dedlem0a 981	Alternate version of dedlema 982. (Contributed by NM, 2-Apr-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
|- ( ph -> ( ps <-> ( ( ch -> ph ) -> ( ps /\ ph ) ) ) )
Theorem	dedlema 982	Lemma for iftrue 3642. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ( ph -> ( ps <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
Theorem	dedlemb 983	Lemma for iffalse 3645. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ( -. ph -> ( ch <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
Theorem	pm4.42r 984	One direction of Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( ( ph /\ ps ) \/ ( ph /\ -. ps ) ) -> ph )
Theorem	ninba 985	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
|- ph   =>    |- ( -. ps -> ( -. ph <-> ( ch /\ ps ) ) )
Theorem	prlem1 986	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.)
|- ( ph -> ( et <-> ch ) )   &    |- ( ps -> -. th )   =>    |- ( ph -> ( ps -> ( ( ( ps /\ ch ) \/ ( th /\ ta ) ) -> et ) ) )
Theorem	prlem2 987	A specialized lemma for set theory (to derive the Axiom of Pairing). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
|- ( ( ( ph /\ ps ) \/ ( ch /\ th ) ) <-> ( ( ph \/ ch ) /\ ( ( ph /\ ps ) \/ ( ch /\ th ) ) ) )
Theorem	oplem1 988	A specialized lemma for set theory (ordered pair theorem). (Contributed by NM, 18-Oct-1995.) (Proof shortened by Wolf Lammen, 8-Dec-2012.) (Proof shortened by Mario Carneiro, 2-Feb-2015.)
|- ( ph -> ( ps \/ ch ) )   &    |- ( ph -> ( th \/ ta ) )   &    |- ( ps <-> th )   &    |- ( ch -> ( th <-> ta ) )   =>    |- ( ph -> ps )
Theorem	rnlem 989	Lemma used in construction of real numbers. (Contributed by NM, 4-Sep-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ( ph /\ ch ) /\ ( ps /\ th ) ) /\ ( ( ph /\ th ) /\ ( ps /\ ch ) ) ) )
1.2.11  The conditional operator for propositions This subsection introduces the conditional operator for propositions, denoted by if- ( ph , ps , ch ) (see df-ifp 991). It is the analogue for propositions of the conditional operator for classes, denoted by if ( ph , A , B ) (see df-if 3636).
Syntax	wif 990	Extend wff notation to include the conditional operator for propositions.
wff if- ( ph , ps , ch )
Definition	df-ifp 991	Definition of the conditional operator for propositions. The expression if- ( ph , ps , ch ) is read "if ph then ps else ch". See dfifp2dc 994, dfifp3dc 995, dfifp4dc 996 and dfifp5dc 997 for alternate definitions. This definition (in the form of dfifp2dc 994) appears in Section II.24 of [Church] p. 129 (Definition D12 page 132), where it is called "conditioned disjunction". Church's [ ps , ph , ch ] corresponds to our if- ( ph , ps , ch ) (note the permutation of the first two variables). This form was chosen as the definition rather than dfifp2dc 994 for compatibility with intuitionistic logic development: with this form, it is clear that if- ( ph , ps , ch ) implies decidability of ph (ifpdc 992), which is most often what is wanted. (Contributed by BJ, 22-Jun-2019.)
|- (if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
Theorem	ifpdc 992	The conditional operator for propositions implies decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
|- (if- ( ph , ps , ch ) -> DECID ph )
Theorem	ifp2 993	Forward direction of dfifp2dc 994. This direction does not require decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
|- (if- ( ph , ps , ch ) -> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )
Theorem	dfifp2dc 994	Alternate definition of the conditional operator for decidable propositions. The value of if- ( ph , ps , ch ) is "if ph then ps, and if not ph then ch". This is the definition used in Section II.24 of [Church] p. 129 (Definition D12 page 132) (see comment of df-ifp 991). (Contributed by BJ, 22-Jun-2019.)
|- (DECID ph -> (if- ( ph , ps , ch ) <-> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) ) )
Theorem	dfifp3dc 995	Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.)
|- (DECID ph -> (if- ( ph , ps , ch ) <-> ( ( ph -> ps ) /\ ( ph \/ ch ) ) ) )
Theorem	dfifp4dc 996	Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.)
|- (DECID ph -> (if- ( ph , ps , ch ) <-> ( ( -. ph \/ ps ) /\ ( ph \/ ch ) ) ) )
Theorem	dfifp5dc 997	Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.)
|- (DECID ph -> (if- ( ph , ps , ch ) <-> ( ( -. ph \/ ps ) /\ ( -. ph -> ch ) ) ) )
Theorem	ifpdfbidc 998	Define the biconditional as conditional logic operator. (Contributed by RP, 20-Apr-2020.) (Proof shortened by Wolf Lammen, 30-Apr-2024.)
|- (DECID ph -> ( ( ph <-> ps ) <-> if- ( ph , ps , -. ps ) ) )
Theorem	anifpdc 999	The conditional operator is implied by the conjunction of its possible outputs. Dual statement of ifpor 1000. (Contributed by BJ, 30-Sep-2019.)
|- (DECID ph -> ( ( ps /\ ch ) -> if- ( ph , ps , ch ) ) )
Theorem	ifpor 1000	The conditional operator implies the disjunction of its possible outputs. Dual statement of anifpdc 999. (Contributed by BJ, 1-Oct-2019.)
|- (if- ( ph , ps , ch ) -> ( ps \/ ch ) )