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 | dcan 934 |
A conjunction of two decidable propositions is decidable. (Contributed by
Jim Kingdon, 12-Apr-2018.)
|
⊢ ((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ∧ 𝜓)) |
|
Theorem | dcan2 935 |
A conjunction of two decidable propositions is decidable, expressed in a
curried form as compared to dcan 934. (Contributed by Jim Kingdon,
12-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 ∧ 𝜓))) |
|
Theorem | dcor 936 |
A disjunction of two decidable propositions is decidable. (Contributed by
Jim Kingdon, 21-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 ∨ 𝜓))) |
|
Theorem | dcbi 937 |
An equivalence of two decidable propositions is decidable. (Contributed
by Jim Kingdon, 12-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 ↔ 𝜓))) |
|
Theorem | annimdc 938 |
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 939 |
Theorem *4.55 of [WhiteheadRussell] p.
120, for decidable propositions.
(Contributed by Jim Kingdon, 2-May-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (¬ 𝜑 ∧ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓)))) |
|
Theorem | orandc 940 |
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 941 |
Detach truth from conjunction in biconditional. (Contributed by NM,
27-Feb-1996.) (Revised by NM, 9-Jan-2015.)
|
⊢ 𝜓
& ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜒) |
|
Theorem | mpbiran2 942 |
Detach truth from conjunction in biconditional. (Contributed by NM,
22-Feb-1996.) (Revised by NM, 9-Jan-2015.)
|
⊢ 𝜒
& ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜓) |
|
Theorem | mpbir2an 943 |
Detach a conjunction of truths in a biconditional. (Contributed by NM,
10-May-2005.) (Revised by NM, 9-Jan-2015.)
|
⊢ 𝜓
& ⊢ 𝜒
& ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ 𝜑 |
|
Theorem | mpbi2and 944 |
Detach a conjunction of truths in a biconditional. (Contributed by NM,
6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) |
|
Theorem | mpbir2and 945 |
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 946 |
Theorem *5.62 of [WhiteheadRussell] p.
125, for a decidable proposition.
(Contributed by Jim Kingdon, 12-May-2018.)
|
⊢ (DECID 𝜓 → (((𝜑 ∧ 𝜓) ∨ ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))) |
|
Theorem | pm5.63dc 947 |
Theorem *5.63 of [WhiteheadRussell] p.
125, for a decidable proposition.
(Contributed by Jim Kingdon, 12-May-2018.)
|
⊢ (DECID 𝜑 → ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ (¬ 𝜑 ∧ 𝜓)))) |
|
Theorem | bianfi 948 |
A wff conjoined with falsehood is false. (Contributed by NM,
5-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
|
⊢ ¬ 𝜑 ⇒ ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑)) |
|
Theorem | bianfd 949 |
A wff conjoined with falsehood is false. (Contributed by NM,
27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.)
|
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) |
|
Theorem | pm4.43 950 |
Theorem *4.43 of [WhiteheadRussell] p.
119. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
|
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ ¬ 𝜓))) |
|
Theorem | pm4.82 951 |
Theorem *4.82 of [WhiteheadRussell] p.
122. (Contributed by NM,
3-Jan-2005.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ ¬ 𝜑) |
|
Theorem | pm4.83dc 952 |
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 953 |
A transitive law of equivalence. Compare Theorem *4.22 of
[WhiteheadRussell] p. 117.
(Contributed by NM, 18-Aug-1993.)
|
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜓)) → (𝜑 ↔ 𝜒)) |
|
Theorem | orbididc 954 |
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 955 |
Disjunction distributes over the biconditional, for a decidable
proposition. Based on theorem *5.7 of [WhiteheadRussell] p. 125. This
theorem is similar to orbididc 954. (Contributed by Jim Kingdon,
2-Apr-2018.)
|
⊢ (DECID 𝜒 → (((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) ↔ (𝜒 ∨ (𝜑 ↔ 𝜓)))) |
|
Theorem | bigolden 956 |
Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by
NM, 10-Jan-2005.)
|
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓))) |
|
Theorem | anordc 957 |
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 958 |
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 959 |
Theorem *3.12 of [WhiteheadRussell] p.
111, but for decidable
propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓)))) |
|
Theorem | pm3.13dc 960 |
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 961 |
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 962 |
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 963 |
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 964 |
Removal of conjunct from one side of an equivalence. (Contributed by NM,
5-Aug-1993.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜒 ↔ (𝜓 ∧ 𝜑))) → (𝜒 ↔ 𝜑)) |
|
Theorem | ccase 965 |
Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
(Proof shortened by Wolf Lammen, 6-Jan-2013.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜏)
& ⊢ ((𝜒 ∧ 𝜓) → 𝜏)
& ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
& ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) |
|
Theorem | ccased 966 |
Deduction for combining cases. (Contributed by NM, 9-May-2004.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂)) |
|
Theorem | ccase2 967 |
Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜏)
& ⊢ (𝜒 → 𝜏)
& ⊢ (𝜃 → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) |
|
Theorem | niabn 968 |
Miscellaneous inference relating falsehoods. (Contributed by NM,
31-Mar-1994.)
|
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → ((𝜒 ∧ 𝜓) ↔ ¬ 𝜑)) |
|
Theorem | dedlem0a 969 |
Alternate version of dedlema 970. (Contributed by NM, 2-Apr-1994.) (Proof
shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen,
4-Dec-2012.)
|
⊢ (𝜑 → (𝜓 ↔ ((𝜒 → 𝜑) → (𝜓 ∧ 𝜑)))) |
|
Theorem | dedlema 970 |
Lemma for iftrue 3551. (Contributed by NM, 26-Jun-2002.) (Proof
shortened
by Andrew Salmon, 7-May-2011.)
|
⊢ (𝜑 → (𝜓 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) |
|
Theorem | dedlemb 971 |
Lemma for iffalse 3554. (Contributed by NM, 15-May-1999.) (Proof
shortened
by Andrew Salmon, 7-May-2011.)
|
⊢ (¬ 𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) |
|
Theorem | pm4.42r 972 |
One direction of Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed
by Jim Kingdon, 4-Aug-2018.)
|
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓)) → 𝜑) |
|
Theorem | ninba 973 |
Miscellaneous inference relating falsehoods. (Contributed by NM,
31-Mar-1994.)
|
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → (¬ 𝜑 ↔ (𝜒 ∧ 𝜓))) |
|
Theorem | prlem1 974 |
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 975 |
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 976 |
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 977 |
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 978 |
Extend wff definition to include 3-way disjunction ('or').
|
wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
|
Syntax | w3a 979 |
Extend wff definition to include 3-way conjunction ('and').
|
wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
|
Definition | df-3or 980 |
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 981 |
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 982 |
Associative law for triple disjunction. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) |
|
Theorem | 3anass 983 |
Associative law for triple conjunction. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) |
|
Theorem | 3anrot 984 |
Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) |
|
Theorem | 3orrot 985 |
Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) |
|
Theorem | 3ancoma 986 |
Commutation law for triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) |
|
Theorem | 3ancomb 987 |
Commutation law for triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
|
Theorem | 3orcomb 988 |
Commutation law for triple disjunction. (Contributed by Scott Fenton,
20-Apr-2011.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓)) |
|
Theorem | 3anrev 989 |
Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓 ∧ 𝜑)) |
|
Theorem | 3anan32 990 |
Convert triple conjunction to conjunction, then commute. (Contributed by
Jonathan Ben-Naim, 3-Jun-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
|
Theorem | 3anan12 991 |
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 992 |
Distribution of triple conjunction over conjunction. (Contributed by
David A. Wheeler, 4-Nov-2018.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) |
|
Theorem | anandi3r 993 |
Distribution of triple conjunction over conjunction. (Contributed by
David A. Wheeler, 4-Nov-2018.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓))) |
|
Theorem | 3ioran 994 |
Negated triple disjunction as triple conjunction. (Contributed by Scott
Fenton, 19-Apr-2011.)
|
⊢ (¬ (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒)) |
|
Theorem | 3simpa 995 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓)) |
|
Theorem | 3simpb 996 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒)) |
|
Theorem | 3simpc 997 |
Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
(Proof shortened by Andrew Salmon, 13-May-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) |
|
Theorem | simp1 998 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) |
|
Theorem | simp2 999 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) |
|
Theorem | simp3 1000 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) |