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