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