Theorem List for Intuitionistic Logic Explorer - 901-1000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | pm5.14dc 901 |
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 902 |
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 903 |
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 904 |
Peirce's theorem for a decidable proposition. This odd-looking theorem
can be seen as an alternative to exmiddc 826, condc 843, or notnotrdc 833 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 905 |
The Inversion Axiom of the infinite-valued sentential logic (L-infinity)
of Lukasiewicz, but where one of the propositions is decidable. Using
dfor2dc 885, 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 906 |
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 907 |
Theorem *5.35 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → 𝜒)) → (𝜑 → (𝜓 ↔ 𝜒))) |
|
Theorem | pm5.54dc 908 |
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 909 |
Move conjunction outside of biconditional. (Contributed by NM,
13-May-1999.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
|
Theorem | baibr 910 |
Move conjunction outside of biconditional. (Contributed by NM,
11-Jul-1994.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜒 ↔ 𝜑)) |
|
Theorem | rbaib 911 |
Move conjunction outside of biconditional. (Contributed by Mario
Carneiro, 11-Sep-2015.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
|
Theorem | rbaibr 912 |
Move conjunction outside of biconditional. (Contributed by Mario
Carneiro, 11-Sep-2015.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜒 → (𝜓 ↔ 𝜑)) |
|
Theorem | baibd 913 |
Move conjunction outside of biconditional. (Contributed by Mario
Carneiro, 11-Sep-2015.)
|
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ↔ 𝜃)) |
|
Theorem | rbaibd 914 |
Move conjunction outside of biconditional. (Contributed by Mario
Carneiro, 11-Sep-2015.)
|
⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜃) → (𝜓 ↔ 𝜒)) |
|
Theorem | pm5.44 915 |
Theorem *5.44 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜒) ↔ (𝜑 → (𝜓 ∧ 𝜒)))) |
|
Theorem | pm5.6dc 916 |
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 917). (Contributed by Jim Kingdon,
2-Apr-2018.)
|
⊢ (DECID 𝜓 → (((𝜑 ∧ ¬ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 ∨ 𝜒)))) |
|
Theorem | pm5.6r 917 |
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 916). (Contributed by Jim Kingdon,
4-Aug-2018.)
|
⊢ ((𝜑 → (𝜓 ∨ 𝜒)) → ((𝜑 ∧ ¬ 𝜓) → 𝜒)) |
|
Theorem | orcanai 918 |
Change disjunction in consequent to conjunction in antecedent.
(Contributed by NM, 8-Jun-1994.)
|
⊢ (𝜑 → (𝜓 ∨ 𝜒)) ⇒ ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜒) |
|
Theorem | intnan 919 |
Introduction of conjunct inside of a contradiction. (Contributed by NM,
16-Sep-1993.)
|
⊢ ¬ 𝜑 ⇒ ⊢ ¬ (𝜓 ∧ 𝜑) |
|
Theorem | intnanr 920 |
Introduction of conjunct inside of a contradiction. (Contributed by NM,
3-Apr-1995.)
|
⊢ ¬ 𝜑 ⇒ ⊢ ¬ (𝜑 ∧ 𝜓) |
|
Theorem | intnand 921 |
Introduction of conjunct inside of a contradiction. (Contributed by NM,
10-Jul-2005.)
|
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ (𝜒 ∧ 𝜓)) |
|
Theorem | intnanrd 922 |
Introduction of conjunct inside of a contradiction. (Contributed by NM,
10-Jul-2005.)
|
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ (𝜓 ∧ 𝜒)) |
|
Theorem | dcan 923 |
A conjunction of two decidable propositions is decidable. (Contributed by
Jim Kingdon, 12-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 ∧ 𝜓))) |
|
Theorem | dcor 924 |
A disjunction of two decidable propositions is decidable. (Contributed by
Jim Kingdon, 21-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 ∨ 𝜓))) |
|
Theorem | dcbi 925 |
An equivalence of two decidable propositions is decidable. (Contributed
by Jim Kingdon, 12-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 ↔ 𝜓))) |
|
Theorem | annimdc 926 |
Express conjunction in terms of implication. The forward direction,
annimim 676, 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 927 |
Theorem *4.55 of [WhiteheadRussell] p.
120, for decidable propositions.
(Contributed by Jim Kingdon, 2-May-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (¬ 𝜑 ∧ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓)))) |
|
Theorem | orandc 928 |
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 929 |
Detach truth from conjunction in biconditional. (Contributed by NM,
27-Feb-1996.) (Revised by NM, 9-Jan-2015.)
|
⊢ 𝜓
& ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜒) |
|
Theorem | mpbiran2 930 |
Detach truth from conjunction in biconditional. (Contributed by NM,
22-Feb-1996.) (Revised by NM, 9-Jan-2015.)
|
⊢ 𝜒
& ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 ↔ 𝜓) |
|
Theorem | mpbir2an 931 |
Detach a conjunction of truths in a biconditional. (Contributed by NM,
10-May-2005.) (Revised by NM, 9-Jan-2015.)
|
⊢ 𝜓
& ⊢ 𝜒
& ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ 𝜑 |
|
Theorem | mpbi2and 932 |
Detach a conjunction of truths in a biconditional. (Contributed by NM,
6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) |
|
Theorem | mpbir2and 933 |
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 934 |
Theorem *5.62 of [WhiteheadRussell] p.
125, for a decidable proposition.
(Contributed by Jim Kingdon, 12-May-2018.)
|
⊢ (DECID 𝜓 → (((𝜑 ∧ 𝜓) ∨ ¬ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))) |
|
Theorem | pm5.63dc 935 |
Theorem *5.63 of [WhiteheadRussell] p.
125, for a decidable proposition.
(Contributed by Jim Kingdon, 12-May-2018.)
|
⊢ (DECID 𝜑 → ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ (¬ 𝜑 ∧ 𝜓)))) |
|
Theorem | bianfi 936 |
A wff conjoined with falsehood is false. (Contributed by NM,
5-Aug-1993.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
|
⊢ ¬ 𝜑 ⇒ ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑)) |
|
Theorem | bianfd 937 |
A wff conjoined with falsehood is false. (Contributed by NM,
27-Mar-1995.) (Proof shortened by Wolf Lammen, 5-Nov-2013.)
|
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒))) |
|
Theorem | pm4.43 938 |
Theorem *4.43 of [WhiteheadRussell] p.
119. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
|
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ ¬ 𝜓))) |
|
Theorem | pm4.82 939 |
Theorem *4.82 of [WhiteheadRussell] p.
122. (Contributed by NM,
3-Jan-2005.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ ¬ 𝜑) |
|
Theorem | pm4.83dc 940 |
Theorem *4.83 of [WhiteheadRussell] p.
122, for decidable propositions.
As with other case elimination theorems, like pm2.61dc 855, it only holds
for decidable propositions. (Contributed by Jim Kingdon, 12-May-2018.)
|
⊢ (DECID 𝜑 → (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜓)) ↔ 𝜓)) |
|
Theorem | biantr 941 |
A transitive law of equivalence. Compare Theorem *4.22 of
[WhiteheadRussell] p. 117.
(Contributed by NM, 18-Aug-1993.)
|
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜓)) → (𝜑 ↔ 𝜒)) |
|
Theorem | orbididc 942 |
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 943 |
Disjunction distributes over the biconditional, for a decidable
proposition. Based on theorem *5.7 of [WhiteheadRussell] p. 125. This
theorem is similar to orbididc 942. (Contributed by Jim Kingdon,
2-Apr-2018.)
|
⊢ (DECID 𝜒 → (((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) ↔ (𝜒 ∨ (𝜑 ↔ 𝜓)))) |
|
Theorem | bigolden 944 |
Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by
NM, 10-Jan-2005.)
|
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓))) |
|
Theorem | anordc 945 |
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 744, holds for all propositions, but the
equivalence only holds given decidability. (Contributed by Jim Kingdon,
21-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ 𝜓) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓)))) |
|
Theorem | pm3.11dc 946 |
Theorem *3.11 of [WhiteheadRussell] p.
111, but for decidable
propositions. The converse, pm3.1 744, holds for all propositions, not
just decidable ones. (Contributed by Jim Kingdon, 22-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (¬ 𝜑 ∨ ¬ 𝜓) → (𝜑 ∧ 𝜓)))) |
|
Theorem | pm3.12dc 947 |
Theorem *3.12 of [WhiteheadRussell] p.
111, but for decidable
propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓)))) |
|
Theorem | pm3.13dc 948 |
Theorem *3.13 of [WhiteheadRussell] p.
111, but for decidable
propositions. The converse, pm3.14 743, holds for all propositions.
(Contributed by Jim Kingdon, 22-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓)))) |
|
Theorem | dn1dc 949 |
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 950 |
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 951 |
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 952 |
Removal of conjunct from one side of an equivalence. (Contributed by NM,
5-Aug-1993.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜒 ↔ (𝜓 ∧ 𝜑))) → (𝜒 ↔ 𝜑)) |
|
Theorem | ccase 953 |
Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
(Proof shortened by Wolf Lammen, 6-Jan-2013.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜏)
& ⊢ ((𝜒 ∧ 𝜓) → 𝜏)
& ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
& ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) |
|
Theorem | ccased 954 |
Deduction for combining cases. (Contributed by NM, 9-May-2004.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂)) |
|
Theorem | ccase2 955 |
Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜏)
& ⊢ (𝜒 → 𝜏)
& ⊢ (𝜃 → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) |
|
Theorem | niabn 956 |
Miscellaneous inference relating falsehoods. (Contributed by NM,
31-Mar-1994.)
|
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → ((𝜒 ∧ 𝜓) ↔ ¬ 𝜑)) |
|
Theorem | dedlem0a 957 |
Alternate version of dedlema 958. (Contributed by NM, 2-Apr-1994.) (Proof
shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen,
4-Dec-2012.)
|
⊢ (𝜑 → (𝜓 ↔ ((𝜒 → 𝜑) → (𝜓 ∧ 𝜑)))) |
|
Theorem | dedlema 958 |
Lemma for iftrue 3520. (Contributed by NM, 26-Jun-2002.) (Proof
shortened
by Andrew Salmon, 7-May-2011.)
|
⊢ (𝜑 → (𝜓 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) |
|
Theorem | dedlemb 959 |
Lemma for iffalse 3523. (Contributed by NM, 15-May-1999.) (Proof
shortened
by Andrew Salmon, 7-May-2011.)
|
⊢ (¬ 𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) |
|
Theorem | pm4.42r 960 |
One direction of Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed
by Jim Kingdon, 4-Aug-2018.)
|
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓)) → 𝜑) |
|
Theorem | ninba 961 |
Miscellaneous inference relating falsehoods. (Contributed by NM,
31-Mar-1994.)
|
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → (¬ 𝜑 ↔ (𝜒 ∧ 𝜓))) |
|
Theorem | prlem1 962 |
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 963 |
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 964 |
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 965 |
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 966 |
Extend wff definition to include 3-way disjunction ('or').
|
wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
|
Syntax | w3a 967 |
Extend wff definition to include 3-way conjunction ('and').
|
wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
|
Definition | df-3or 968 |
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 757. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
|
Definition | df-3an 969 |
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 399. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
|
Theorem | 3orass 970 |
Associative law for triple disjunction. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) |
|
Theorem | 3anass 971 |
Associative law for triple conjunction. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) |
|
Theorem | 3anrot 972 |
Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) |
|
Theorem | 3orrot 973 |
Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) |
|
Theorem | 3ancoma 974 |
Commutation law for triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) |
|
Theorem | 3ancomb 975 |
Commutation law for triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
|
Theorem | 3orcomb 976 |
Commutation law for triple disjunction. (Contributed by Scott Fenton,
20-Apr-2011.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓)) |
|
Theorem | 3anrev 977 |
Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓 ∧ 𝜑)) |
|
Theorem | 3anan32 978 |
Convert triple conjunction to conjunction, then commute. (Contributed by
Jonathan Ben-Naim, 3-Jun-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
|
Theorem | 3anan12 979 |
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 980 |
Distribution of triple conjunction over conjunction. (Contributed by
David A. Wheeler, 4-Nov-2018.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) |
|
Theorem | anandi3r 981 |
Distribution of triple conjunction over conjunction. (Contributed by
David A. Wheeler, 4-Nov-2018.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓))) |
|
Theorem | 3ioran 982 |
Negated triple disjunction as triple conjunction. (Contributed by Scott
Fenton, 19-Apr-2011.)
|
⊢ (¬ (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒)) |
|
Theorem | 3simpa 983 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓)) |
|
Theorem | 3simpb 984 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒)) |
|
Theorem | 3simpc 985 |
Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
(Proof shortened by Andrew Salmon, 13-May-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) |
|
Theorem | simp1 986 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) |
|
Theorem | simp2 987 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) |
|
Theorem | simp3 988 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) |
|
Theorem | simpl1 989 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) |
|
Theorem | simpl2 990 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) |
|
Theorem | simpl3 991 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) |
|
Theorem | simpr1 992 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
|
Theorem | simpr2 993 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒) |
|
Theorem | simpr3 994 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃) |
|
Theorem | simp1i 995 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜑 |
|
Theorem | simp2i 996 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜓 |
|
Theorem | simp3i 997 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜒 |
|
Theorem | simp1d 998 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | simp2d 999 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | simp3d 1000 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) |