Type | Label | Description |
Statement |
|
Theorem | pm4.64dc 901 |
Theorem *4.64 of [WhiteheadRussell] p.
120, given a decidability
condition. The reverse direction, pm2.53 723, holds for all propositions.
(Contributed by Jim Kingdon, 2-May-2018.)
|
⊢ (DECID 𝜑 → ((¬ 𝜑 → 𝜓) ↔ (𝜑 ∨ 𝜓))) |
|
Theorem | pm4.66dc 902 |
Theorem *4.66 of [WhiteheadRussell] p.
120, given a decidability
condition. (Contributed by Jim Kingdon, 2-May-2018.)
|
⊢ (DECID 𝜑 → ((¬ 𝜑 → ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))) |
|
Theorem | pm4.54dc 903 |
Theorem *4.54 of [WhiteheadRussell] p.
120, for decidable propositions.
One form of DeMorgan's law. (Contributed by Jim Kingdon, 2-May-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → ((¬ 𝜑 ∧ 𝜓) ↔ ¬ (𝜑 ∨ ¬ 𝜓)))) |
|
Theorem | pm4.79dc 904 |
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 𝜑 → (DECID 𝜓 → (((𝜓 → 𝜑) ∨ (𝜒 → 𝜑)) ↔ ((𝜓 ∧ 𝜒) → 𝜑)))) |
|
Theorem | pm5.17dc 905 |
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 𝜓 → (((𝜑 ∨ 𝜓) ∧ ¬ (𝜑 ∧ 𝜓)) ↔ (𝜑 ↔ ¬ 𝜓))) |
|
Theorem | pm2.85dc 906 |
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 𝜑 → (((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)) → (𝜑 ∨ (𝜓 → 𝜒)))) |
|
Theorem | orimdidc 907 |
Disjunction distributes over implication. The forward direction,
pm2.76 809, is valid intuitionistically. The reverse
direction holds if
𝜑 is decidable, as can be seen at pm2.85dc 906. (Contributed by Jim
Kingdon, 1-Apr-2018.)
|
⊢ (DECID 𝜑 → ((𝜑 ∨ (𝜓 → 𝜒)) ↔ ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)))) |
|
Theorem | pm2.26dc 908 |
Decidable proposition version of theorem *2.26 of [WhiteheadRussell]
p. 104. (Contributed by Jim Kingdon, 20-Apr-2018.)
|
⊢ (DECID 𝜑 → (¬ 𝜑 ∨ ((𝜑 → 𝜓) → 𝜓))) |
|
Theorem | pm4.81dc 909 |
Theorem *4.81 of [WhiteheadRussell] p.
122, for decidable propositions.
This one needs a decidability condition, but compare with pm4.8 708
which
holds for all propositions. (Contributed by Jim Kingdon, 4-Jul-2018.)
|
⊢ (DECID 𝜑 → ((¬ 𝜑 → 𝜑) ↔ 𝜑)) |
|
Theorem | pm5.11dc 910 |
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 𝜑 → (DECID 𝜓 → ((𝜑 → 𝜓) ∨ (¬ 𝜑 → 𝜓)))) |
|
Theorem | pm5.12dc 911 |
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 𝜓 → ((𝜑 → 𝜓) ∨ (𝜑 → ¬ 𝜓))) |
|
Theorem | pm5.14dc 912 |
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 𝜓 → ((𝜑 → 𝜓) ∨ (𝜓 → 𝜒))) |
|
Theorem | pm5.13dc 913 |
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 𝜓 → ((𝜑 → 𝜓) ∨ (𝜓 → 𝜑))) |
|
Theorem | pm5.55dc 914 |
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 𝜑 → (((𝜑 ∨ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∨ 𝜓) ↔ 𝜓))) |
|
Theorem | peircedc 915 |
Peirce's theorem for a decidable proposition. This odd-looking theorem
can be seen as an alternative to exmiddc 837, condc 854, or notnotrdc 844 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 𝜑 → (((𝜑 → 𝜓) → 𝜑) → 𝜑)) |
|
Theorem | looinvdc 916 |
The Inversion Axiom of the infinite-valued sentential logic (L-infinity)
of Lukasiewicz, but where one of the propositions is decidable. Using
dfor2dc 896, 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 𝜑 → (((𝜑 → 𝜓) → 𝜓) → ((𝜓 → 𝜑) → 𝜑))) |
|
1.2.10 Miscellaneous theorems of propositional
calculus
|
|
Theorem | pm5.21nd 917 |
Eliminate an antecedent implied by each side of a biconditional.
(Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen,
4-Nov-2013.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜃)
& ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
& ⊢ (𝜃 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
|
Theorem | pm5.35 918 |
Theorem *5.35 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ↔ 𝜒))) |
|
Theorem | pm5.54dc 919 |
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 𝜑 → (((𝜑 ∧ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∧ 𝜓) ↔ 𝜓))) |
|
Theorem | baib 920 |
Move conjunction outside of biconditional. (Contributed by NM,
13-May-1999.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
|
Theorem | baibr 921 |
Move conjunction outside of biconditional. (Contributed by NM,
11-Jul-1994.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜒 ↔ 𝜑)) |
|
Theorem | rbaib 922 |
Move conjunction outside of biconditional. (Contributed by Mario
Carneiro, 11-Sep-2015.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
|
Theorem | rbaibr 923 |
Move conjunction outside of biconditional. (Contributed by Mario
Carneiro, 11-Sep-2015.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜒 → (𝜓 ↔ 𝜑)) |
|
Theorem | baibd 924 |
Move conjunction outside of biconditional. (Contributed by Mario
Carneiro, 11-Sep-2015.)
|
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃)) |
|
Theorem | rbaibd 925 |
Move conjunction outside of biconditional. (Contributed by Mario
Carneiro, 11-Sep-2015.)
|
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) |
|
Theorem | pm5.44 926 |
Theorem *5.44 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜒) ↔ (𝜑 → (𝜓 ∧ 𝜒)))) |
|
Theorem | pm5.6dc 927 |
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 928). (Contributed by Jim Kingdon,
2-Apr-2018.)
|
⊢ (DECID 𝜓 → (((𝜑 ∧ ¬ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 ∨ 𝜒)))) |
|
Theorem | pm5.6r 928 |
Conjunction in antecedent versus disjunction in consequent. One direction
of Theorem *5.6 of [WhiteheadRussell] p. 125. If 𝜓 is
decidable, the
converse also holds (see pm5.6dc 927). (Contributed by Jim Kingdon,
4-Aug-2018.)
|
⊢ ((𝜑 → (𝜓 ∨ 𝜒)) → ((𝜑 ∧ ¬ 𝜓) → 𝜒)) |
|
Theorem | orcanai 929 |
Change disjunction in consequent to conjunction in antecedent.
(Contributed by NM, 8-Jun-1994.)
|
⊢ (𝜑 → (𝜓 ∨ 𝜒)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) |
|
Theorem | intnan 930 |
Introduction of conjunct inside of a contradiction. (Contributed by NM,
16-Sep-1993.)
|
⊢ ¬ 𝜑 ⇒ ⊢ ¬ (𝜓 ∧ 𝜑) |
|
Theorem | intnanr 931 |
Introduction of conjunct inside of a contradiction. (Contributed by NM,
3-Apr-1995.)
|
⊢ ¬ 𝜑 ⇒ ⊢ ¬ (𝜑 ∧ 𝜓) |
|
Theorem | intnand 932 |
Introduction of conjunct inside of a contradiction. (Contributed by NM,
10-Jul-2005.)
|
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓)) |
|
Theorem | intnanrd 933 |
Introduction of conjunct inside of a contradiction. (Contributed by NM,
10-Jul-2005.)
|
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) |
|
Theorem | dcand 934 |
A conjunction of two decidable propositions is decidable. (Contributed
by Jim Kingdon, 12-Apr-2018.) (Revised by BJ, 14-Nov-2024.)
|
⊢ (𝜑 → DECID 𝜓) & ⊢ (𝜑 → DECID
𝜒)
⇒ ⊢ (𝜑 → DECID (𝜓 ∧ 𝜒)) |
|
Theorem | dcan 935 |
A conjunction of two decidable propositions is decidable. (Contributed by
Jim Kingdon, 12-Apr-2018.)
|
⊢ ((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ∧ 𝜓)) |
|
Theorem | dcan2 936 |
A conjunction of two decidable propositions is decidable, expressed in a
curried form as compared to dcan 935. 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 𝜑 → (DECID 𝜓 → DECID
(𝜑 ∧ 𝜓))) |
|
Theorem | dcor 937 |
A disjunction of two decidable propositions is decidable. (Contributed by
Jim Kingdon, 21-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 ∨ 𝜓))) |
|
Theorem | dcbi 938 |
An equivalence of two decidable propositions is decidable. (Contributed
by Jim Kingdon, 12-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 ↔ 𝜓))) |
|
Theorem | annimdc 939 |
Express conjunction in terms of implication. The forward direction,
annimim 687, is valid for all propositions, but as an
equivalence, it
requires a decidability condition. (Contributed by Jim Kingdon,
25-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)))) |
|
Theorem | pm4.55dc 940 |
Theorem *4.55 of [WhiteheadRussell] p.
120, for decidable propositions.
(Contributed by Jim Kingdon, 2-May-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (¬ 𝜑 ∧ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓)))) |
|
Theorem | orandc 941 |
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 𝜑 ∧ DECID 𝜓) → ((𝜑 ∨ 𝜓) ↔ ¬ (¬ 𝜑 ∧ ¬ 𝜓))) |
|
Theorem | mpbiran 942 |
Detach truth from conjunction in biconditional. (Contributed by NM,
27-Feb-1996.) (Revised by NM, 9-Jan-2015.)
|
⊢ 𝜓
& ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜒) |
|
Theorem | mpbiran2 943 |
Detach truth from conjunction in biconditional. (Contributed by NM,
22-Feb-1996.) (Revised by NM, 9-Jan-2015.)
|
⊢ 𝜒
& ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜓) |
|
Theorem | mpbir2an 944 |
Detach a conjunction of truths in a biconditional. (Contributed by NM,
10-May-2005.) (Revised by NM, 9-Jan-2015.)
|
⊢ 𝜓
& ⊢ 𝜒
& ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ 𝜑 |
|
Theorem | mpbi2and 945 |
Detach a conjunction of truths in a biconditional. (Contributed by NM,
6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) |
|
Theorem | mpbir2and 946 |
Detach a conjunction of truths in a biconditional. (Contributed by NM,
6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | pm5.62dc 947 |
Theorem *5.62 of [WhiteheadRussell] p.
125, for a decidable proposition.
(Contributed by Jim Kingdon, 12-May-2018.)
|
⊢ (DECID 𝜓 → (((𝜑 ∧ 𝜓) ∨ ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))) |
|
Theorem | pm5.63dc 948 |
Theorem *5.63 of [WhiteheadRussell] p.
125, for a decidable proposition.
(Contributed by Jim Kingdon, 12-May-2018.)
|
⊢ (DECID 𝜑 → ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ (¬ 𝜑 ∧ 𝜓)))) |
|
Theorem | bianfi 949 |
A wff conjoined with falsehood is false. (Contributed by NM,
5-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
|
⊢ ¬ 𝜑 ⇒ ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑)) |
|
Theorem | bianfd 950 |
A wff conjoined with falsehood is false. (Contributed by NM,
27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.)
|
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) |
|
Theorem | pm4.43 951 |
Theorem *4.43 of [WhiteheadRussell] p.
119. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
|
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ ¬ 𝜓))) |
|
Theorem | pm4.82 952 |
Theorem *4.82 of [WhiteheadRussell] p.
122. (Contributed by NM,
3-Jan-2005.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ ¬ 𝜑) |
|
Theorem | pm4.83dc 953 |
Theorem *4.83 of [WhiteheadRussell] p.
122, for decidable propositions.
As with other case elimination theorems, like pm2.61dc 866, it only holds
for decidable propositions. (Contributed by Jim Kingdon, 12-May-2018.)
|
⊢ (DECID 𝜑 → (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜓)) ↔ 𝜓)) |
|
Theorem | biantr 954 |
A transitive law of equivalence. Compare Theorem *4.22 of
[WhiteheadRussell] p. 117.
(Contributed by NM, 18-Aug-1993.)
|
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜓)) → (𝜑 ↔ 𝜒)) |
|
Theorem | orbididc 955 |
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 𝜑 → ((𝜑 ∨ (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ 𝜒)))) |
|
Theorem | pm5.7dc 956 |
Disjunction distributes over the biconditional, for a decidable
proposition. Based on theorem *5.7 of [WhiteheadRussell] p. 125. This
theorem is similar to orbididc 955. (Contributed by Jim Kingdon,
2-Apr-2018.)
|
⊢ (DECID 𝜒 → (((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) ↔ (𝜒 ∨ (𝜑 ↔ 𝜓)))) |
|
Theorem | bigolden 957 |
Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by
NM, 10-Jan-2005.)
|
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓))) |
|
Theorem | anordc 958 |
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 755, holds for all propositions, but the
equivalence only holds given decidability. (Contributed by Jim Kingdon,
21-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ 𝜓) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓)))) |
|
Theorem | pm3.11dc 959 |
Theorem *3.11 of [WhiteheadRussell] p.
111, but for decidable
propositions. The converse, pm3.1 755, holds for all propositions, not
just decidable ones. (Contributed by Jim Kingdon, 22-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (¬ 𝜑 ∨ ¬ 𝜓) → (𝜑 ∧ 𝜓)))) |
|
Theorem | pm3.12dc 960 |
Theorem *3.12 of [WhiteheadRussell] p.
111, but for decidable
propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓)))) |
|
Theorem | pm3.13dc 961 |
Theorem *3.13 of [WhiteheadRussell] p.
111, but for decidable
propositions. The converse, pm3.14 754, holds for all propositions.
(Contributed by Jim Kingdon, 22-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓)))) |
|
Theorem | dn1dc 962 |
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 𝜑 ∧ (DECID 𝜓 ∧ (DECID
𝜒 ∧ DECID
𝜃))) → (¬ (¬
(¬ (𝜑 ∨ 𝜓) ∨ 𝜒) ∨ ¬ (𝜑 ∨ ¬ (¬ 𝜒 ∨ ¬ (𝜒 ∨ 𝜃)))) ↔ 𝜒)) |
|
Theorem | pm5.71dc 963 |
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 𝜓 → ((𝜓 → ¬ 𝜒) → (((𝜑 ∨ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ 𝜒)))) |
|
Theorem | pm5.75 964 |
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.)
|
⊢ (((𝜒 → ¬ 𝜓) ∧ (𝜑 ↔ (𝜓 ∨ 𝜒))) → ((𝜑 ∧ ¬ 𝜓) ↔ 𝜒)) |
|
Theorem | bimsc1 965 |
Removal of conjunct from one side of an equivalence. (Contributed by NM,
5-Aug-1993.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜒 ↔ (𝜓 ∧ 𝜑))) → (𝜒 ↔ 𝜑)) |
|
Theorem | ccase 966 |
Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
(Proof shortened by Wolf Lammen, 6-Jan-2013.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜏)
& ⊢ ((𝜒 ∧ 𝜓) → 𝜏)
& ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
& ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) |
|
Theorem | ccased 967 |
Deduction for combining cases. (Contributed by NM, 9-May-2004.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂)) |
|
Theorem | ccase2 968 |
Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜏)
& ⊢ (𝜒 → 𝜏)
& ⊢ (𝜃 → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) |
|
Theorem | niabn 969 |
Miscellaneous inference relating falsehoods. (Contributed by NM,
31-Mar-1994.)
|
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → ((𝜒 ∧ 𝜓) ↔ ¬ 𝜑)) |
|
Theorem | dedlem0a 970 |
Alternate version of dedlema 971. (Contributed by NM, 2-Apr-1994.) (Proof
shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen,
4-Dec-2012.)
|
⊢ (𝜑 → (𝜓 ↔ ((𝜒 → 𝜑) → (𝜓 ∧ 𝜑)))) |
|
Theorem | dedlema 971 |
Lemma for iftrue 3554. (Contributed by NM, 26-Jun-2002.) (Proof
shortened
by Andrew Salmon, 7-May-2011.)
|
⊢ (𝜑 → (𝜓 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) |
|
Theorem | dedlemb 972 |
Lemma for iffalse 3557. (Contributed by NM, 15-May-1999.) (Proof
shortened
by Andrew Salmon, 7-May-2011.)
|
⊢ (¬ 𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) |
|
Theorem | pm4.42r 973 |
One direction of Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed
by Jim Kingdon, 4-Aug-2018.)
|
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓)) → 𝜑) |
|
Theorem | ninba 974 |
Miscellaneous inference relating falsehoods. (Contributed by NM,
31-Mar-1994.)
|
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → (¬ 𝜑 ↔ (𝜒 ∧ 𝜓))) |
|
Theorem | prlem1 975 |
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 976 |
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.)
|
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∧ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ 𝜃)))) |
|
Theorem | oplem1 977 |
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.)
|
⊢ (𝜑 → (𝜓 ∨ 𝜒)) & ⊢ (𝜑 → (𝜃 ∨ 𝜏)) & ⊢ (𝜓 ↔ 𝜃)
& ⊢ (𝜒 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | rnlem 978 |
Lemma used in construction of real numbers. (Contributed by NM,
4-Sep-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜒)))) |
|
1.2.11 Abbreviated conjunction and disjunction of
three wff's
|
|
Syntax | w3o 979 |
Extend wff definition to include 3-way disjunction ('or').
|
wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
|
Syntax | w3a 980 |
Extend wff definition to include 3-way conjunction ('and').
|
wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
|
Definition | df-3or 981 |
Define disjunction ('or') of 3 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 768. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
|
Definition | df-3an 982 |
Define conjunction ('and') of 3 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 401. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
|
Theorem | 3orass 983 |
Associative law for triple disjunction. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) |
|
Theorem | 3anass 984 |
Associative law for triple conjunction. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) |
|
Theorem | 3anrot 985 |
Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) |
|
Theorem | 3orrot 986 |
Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) |
|
Theorem | 3ancoma 987 |
Commutation law for triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) |
|
Theorem | 3ancomb 988 |
Commutation law for triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
|
Theorem | 3orcomb 989 |
Commutation law for triple disjunction. (Contributed by Scott Fenton,
20-Apr-2011.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓)) |
|
Theorem | 3anrev 990 |
Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓 ∧ 𝜑)) |
|
Theorem | 3anan32 991 |
Convert triple conjunction to conjunction, then commute. (Contributed by
Jonathan Ben-Naim, 3-Jun-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
|
Theorem | 3anan12 992 |
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 993 |
Distribution of triple conjunction over conjunction. (Contributed by
David A. Wheeler, 4-Nov-2018.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) |
|
Theorem | anandi3r 994 |
Distribution of triple conjunction over conjunction. (Contributed by
David A. Wheeler, 4-Nov-2018.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓))) |
|
Theorem | 3ioran 995 |
Negated triple disjunction as triple conjunction. (Contributed by Scott
Fenton, 19-Apr-2011.)
|
⊢ (¬ (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒)) |
|
Theorem | 3simpa 996 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓)) |
|
Theorem | 3simpb 997 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒)) |
|
Theorem | 3simpc 998 |
Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
(Proof shortened by Andrew Salmon, 13-May-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) |
|
Theorem | simp1 999 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) |
|
Theorem | simp2 1000 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) |