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	pm2.68dc 901	Concluding disjunction from implication for a decidable proposition. Based on theorem *2.68 of [WhiteheadRussell] p. 108. Converse of pm2.62 755 and one half of dfor2dc 902. (Contributed by Jim Kingdon, 27-Mar-2018.)
|- (DECID ph -> ( ( ( ph -> ps ) -> ps ) -> ( ph \/ ps ) ) )
Theorem	dfor2dc 902	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 903	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 904	Implication in terms of disjunction for a decidable proposition. Based on theorem *4.6 of [WhiteheadRussell] p. 120. The reverse direction, imorr 728, holds for all propositions. (Contributed by Jim Kingdon, 20-Apr-2018.)
|- (DECID ph -> ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) )
Theorem	pm4.62dc 905	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 906	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 760, 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 907	Theorem *4.64 of [WhiteheadRussell] p. 120, given a decidability condition. The reverse direction, pm2.53 729, holds for all propositions. (Contributed by Jim Kingdon, 2-May-2018.)
|- (DECID ph -> ( ( -. ph -> ps ) <-> ( ph \/ ps ) ) )
Theorem	pm4.66dc 908	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 909	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 910	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 911	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 912	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 913	Disjunction distributes over implication. The forward direction, pm2.76 815, is valid intuitionistically. The reverse direction holds if ph is decidable, as can be seen at pm2.85dc 912. (Contributed by Jim Kingdon, 1-Apr-2018.)
|- (DECID ph -> ( ( ph \/ ( ps -> ch ) ) <-> ( ( ph \/ ps ) -> ( ph \/ ch ) ) ) )
Theorem	pm2.26dc 914	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 915	Theorem *4.81 of [WhiteheadRussell] p. 122, for decidable propositions. This one needs a decidability condition, but compare with pm4.8 714 which holds for all propositions. (Contributed by Jim Kingdon, 4-Jul-2018.)
|- (DECID ph -> ( ( -. ph -> ph ) <-> ph ) )
Theorem	pm5.11dc 916	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 917	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 918	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 919	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 920	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 921	Peirce's theorem for a decidable proposition. This odd-looking theorem can be seen as an alternative to exmiddc 843, condc 860, or notnotrdc 850 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 922	The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz, but where one of the propositions is decidable. Using dfor2dc 902, 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  Miscellaneous theorems of propositional calculus
Theorem	pm5.21nd 923	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 924	Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) -> ( ph -> ( ps <-> ch ) ) )
Theorem	pm5.54dc 925	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 926	Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ph <-> ch ) )
Theorem	baibr 927	Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ps -> ( ch <-> ph ) )
Theorem	rbaib 928	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ch -> ( ph <-> ps ) )
Theorem	rbaibr 929	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph <-> ( ps /\ ch ) )   =>    |- ( ch -> ( ps <-> ph ) )
Theorem	baibd 930	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ ch ) -> ( ps <-> th ) )
Theorem	rbaibd 931	Move conjunction outside of biconditional. (Contributed by Mario Carneiro, 11-Sep-2015.)
|- ( ph -> ( ps <-> ( ch /\ th ) ) )   =>    |- ( ( ph /\ th ) -> ( ps <-> ch ) )
Theorem	pm5.44 932	Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
|- ( ( ph -> ps ) -> ( ( ph -> ch ) <-> ( ph -> ( ps /\ ch ) ) ) )
Theorem	pm5.6dc 933	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 934). (Contributed by Jim Kingdon, 2-Apr-2018.)
|- (DECID ps -> ( ( ( ph /\ -. ps ) -> ch ) <-> ( ph -> ( ps \/ ch ) ) ) )
Theorem	pm5.6r 934	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 933). (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( ph -> ( ps \/ ch ) ) -> ( ( ph /\ -. ps ) -> ch ) )
Theorem	orcanai 935	Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
|- ( ph -> ( ps \/ ch ) )   =>    |- ( ( ph /\ -. ps ) -> ch )
Theorem	intnan 936	Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
|- -. ph   =>    |- -. ( ps /\ ph )
Theorem	intnanr 937	Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
|- -. ph   =>    |- -. ( ph /\ ps )
Theorem	intnand 938	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. ( ch /\ ps ) )
Theorem	intnanrd 939	Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. ( ps /\ ch ) )
Theorem	dcand 940	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 941	A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
|- ( (DECID ph /\ DECID ps ) -> DECID ( ph /\ ps ) )
Theorem	dcan2 942	A conjunction of two decidable propositions is decidable, expressed in a curried form as compared to dcan 941. 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 943	A disjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.)
|- (DECID ph -> (DECID ps -> DECID ( ph \/ ps ) ) )
Theorem	dcbi 944	An equivalence of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
|- (DECID ph -> (DECID ps -> DECID ( ph <-> ps ) ) )
Theorem	annimdc 945	Express conjunction in terms of implication. The forward direction, annimim 692, 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 946	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 947	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 948	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 949	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 950	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 951	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 952	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 953	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 954	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 955	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 956	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 957	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 958	Theorem *4.82 of [WhiteheadRussell] p. 122. (Contributed by NM, 3-Jan-2005.)
|- ( ( ( ph -> ps ) /\ ( ph -> -. ps ) ) <-> -. ph )
Theorem	pm4.83dc 959	Theorem *4.83 of [WhiteheadRussell] p. 122, for decidable propositions. As with other case elimination theorems, like pm2.61dc 872, it only holds for decidable propositions. (Contributed by Jim Kingdon, 12-May-2018.)
|- (DECID ph -> ( ( ( ph -> ps ) /\ ( -. ph -> ps ) ) <-> ps ) )
Theorem	biantr 960	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 961	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 962	Disjunction distributes over the biconditional, for a decidable proposition. Based on theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbididc 961. (Contributed by Jim Kingdon, 2-Apr-2018.)
|- (DECID ch -> ( ( ( ph \/ ch ) <-> ( ps \/ ch ) ) <-> ( ch \/ ( ph <-> ps ) ) ) )
Theorem	bigolden 963	Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by NM, 10-Jan-2005.)
|- ( ( ( ph /\ ps ) <-> ph ) <-> ( ps <-> ( ph \/ ps ) ) )
Theorem	anordc 964	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 761, 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 965	Theorem *3.11 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.1 761, 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 966	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 967	Theorem *3.13 of [WhiteheadRussell] p. 111, but for decidable propositions. The converse, pm3.14 760, holds for all propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
|- (DECID ph -> (DECID ps -> ( -. ( ph /\ ps ) -> ( -. ph \/ -. ps ) ) ) )
Theorem	dn1dc 968	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 969	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 970	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 971	Removal of conjunct from one side of an equivalence. (Contributed by NM, 5-Aug-1993.)
|- ( ( ( ph -> ps ) /\ ( ch <-> ( ps /\ ph ) ) ) -> ( ch <-> ph ) )
Theorem	ccase 972	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 973	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 974	Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
|- ( ( ph /\ ps ) -> ta )   &    |- ( ch -> ta )   &    |- ( th -> ta )   =>    |- ( ( ( ph \/ ch ) /\ ( ps \/ th ) ) -> ta )
Theorem	niabn 975	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
|- ph   =>    |- ( -. ps -> ( ( ch /\ ps ) <-> -. ph ) )
Theorem	dedlem0a 976	Alternate version of dedlema 977. (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 977	Lemma for iftrue 3610. (Contributed by NM, 26-Jun-2002.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ( ph -> ( ps <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
Theorem	dedlemb 978	Lemma for iffalse 3613. (Contributed by NM, 15-May-1999.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ( -. ph -> ( ch <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
Theorem	pm4.42r 979	One direction of Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed by Jim Kingdon, 4-Aug-2018.)
|- ( ( ( ph /\ ps ) \/ ( ph /\ -. ps ) ) -> ph )
Theorem	ninba 980	Miscellaneous inference relating falsehoods. (Contributed by NM, 31-Mar-1994.)
|- ph   =>    |- ( -. ps -> ( -. ph <-> ( ch /\ ps ) ) )
Theorem	prlem1 981	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 982	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 983	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 984	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 986). It is the analogue for propositions of the conditional operator for classes, denoted by if ( ph , A , B ) (see df-if 3606).
Syntax	wif 985	Extend wff notation to include the conditional operator for propositions.
wff if- ( ph , ps , ch )
Definition	df-ifp 986	Definition of the conditional operator for propositions. The expression if- ( ph , ps , ch ) is read "if ph then ps else ch". See dfifp2dc 989, dfifp3dc 990, dfifp4dc 991 and dfifp5dc 992 for alternate definitions. This definition (in the form of dfifp2dc 989) 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 989 for compatibility with intuitionistic logic development: with this form, it is clear that if- ( ph , ps , ch ) implies decidability of ph (ifpdc 987), which is most often what is wanted. (Contributed by BJ, 22-Jun-2019.)
|- (if- ( ph , ps , ch ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
Theorem	ifpdc 987	The conditional operator for propositions implies decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
|- (if- ( ph , ps , ch ) -> DECID ph )
Theorem	ifp2 988	Forward direction of dfifp2dc 989. This direction does not require decidability. (Contributed by Jim Kingdon, 25-Jan-2026.)
|- (if- ( ph , ps , ch ) -> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) )
Theorem	dfifp2dc 989	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 986). (Contributed by BJ, 22-Jun-2019.)
|- (DECID ph -> (if- ( ph , ps , ch ) <-> ( ( ph -> ps ) /\ ( -. ph -> ch ) ) ) )
Theorem	dfifp3dc 990	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 991	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 992	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 993	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 994	The conditional operator is implied by the conjunction of its possible outputs. Dual statement of ifpor 995. (Contributed by BJ, 30-Sep-2019.)
|- (DECID ph -> ( ( ps /\ ch ) -> if- ( ph , ps , ch ) ) )
Theorem	ifpor 995	The conditional operator implies the disjunction of its possible outputs. Dual statement of anifpdc 994. (Contributed by BJ, 1-Oct-2019.)
|- (if- ( ph , ps , ch ) -> ( ps \/ ch ) )
Theorem	ifpnst 996	Conditional operator for the negation of a proposition. (Contributed by BJ, 30-Sep-2019.) (Proof shortened by Wolf Lammen, 5-May-2024.)
|- (STAB ph -> (if- ( ph , ps , ch ) <-> if- ( -. ph , ch , ps ) ) )
Theorem	ifptru 997	Value of the conditional operator for propositions when its first argument is true. Analogue for propositions of iftrue 3610. This is essentially dedlema 977. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 10-Jul-2020.)
|- ( ph -> (if- ( ph , ps , ch ) <-> ps ) )
Theorem	ifpfal 998	Value of the conditional operator for propositions when its first argument is false. Analogue for propositions of iffalse 3613. This is essentially dedlemb 978. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 25-Jun-2020.)
|- ( -. ph -> (if- ( ph , ps , ch ) <-> ch ) )
Theorem	ifpiddc 999	Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of ifiddc 3641. (Contributed by BJ, 20-Sep-2019.)
|- (DECID ph -> (if- ( ph , ps , ps ) <-> ps ) )
Theorem	ifpbi123d 1000	Equivalence deduction for conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 17-Apr-2024.)
|- ( ph -> ( ps <-> ta ) )   &    |- ( ph -> ( ch <-> et ) )   &    |- ( ph -> ( th <-> ze ) )   =>    |- ( ph -> (if- ( ps , ch , th ) <-> if- ( ta , et , ze ) ) )