Theorem List for Intuitionistic Logic Explorer - 901-1000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | pm4.43 901 |
Theorem *4.43 of [WhiteheadRussell] p.
119. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 26-Nov-2012.)
|
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ ¬ 𝜓))) |
|
Theorem | pm4.82 902 |
Theorem *4.82 of [WhiteheadRussell] p.
122. (Contributed by NM,
3-Jan-2005.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜑 → ¬ 𝜓)) ↔ ¬ 𝜑) |
|
Theorem | pm4.83dc 903 |
Theorem *4.83 of [WhiteheadRussell] p.
122, for decidable propositions.
As with other case elimination theorems, like pm2.61dc 806, it only holds
for decidable propositions. (Contributed by Jim Kingdon, 12-May-2018.)
|
⊢ (DECID 𝜑 → (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜓)) ↔ 𝜓)) |
|
Theorem | biantr 904 |
A transitive law of equivalence. Compare Theorem *4.22 of
[WhiteheadRussell] p. 117.
(Contributed by NM, 18-Aug-1993.)
|
⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜓)) → (𝜑 ↔ 𝜒)) |
|
Theorem | orbididc 905 |
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 906 |
Disjunction distributes over the biconditional, for a decidable
proposition. Based on theorem *5.7 of [WhiteheadRussell] p. 125. This
theorem is similar to orbididc 905. (Contributed by Jim Kingdon,
2-Apr-2018.)
|
⊢ (DECID 𝜒 → (((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) ↔ (𝜒 ∨ (𝜑 ↔ 𝜓)))) |
|
Theorem | bigolden 907 |
Dijkstra-Scholten's Golden Rule for calculational proofs. (Contributed by
NM, 10-Jan-2005.)
|
⊢ (((𝜑 ∧ 𝜓) ↔ 𝜑) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓))) |
|
Theorem | anordc 908 |
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 712, holds for all propositions, but the
equivalence only holds given decidability. (Contributed by Jim Kingdon,
21-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ 𝜓) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓)))) |
|
Theorem | pm3.11dc 909 |
Theorem *3.11 of [WhiteheadRussell] p.
111, but for decidable
propositions. The converse, pm3.1 712, holds for all propositions, not
just decidable ones. (Contributed by Jim Kingdon, 22-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (¬ 𝜑 ∨ ¬ 𝜓) → (𝜑 ∧ 𝜓)))) |
|
Theorem | pm3.12dc 910 |
Theorem *3.12 of [WhiteheadRussell] p.
111, but for decidable
propositions. (Contributed by Jim Kingdon, 22-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓)))) |
|
Theorem | pm3.13dc 911 |
Theorem *3.13 of [WhiteheadRussell] p.
111, but for decidable
propositions. The converse, pm3.14 711, holds for all propositions.
(Contributed by Jim Kingdon, 22-Apr-2018.)
|
⊢ (DECID 𝜑 → (DECID 𝜓 → (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓)))) |
|
Theorem | dn1dc 912 |
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 913 |
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 914 |
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 915 |
Removal of conjunct from one side of an equivalence. (Contributed by NM,
5-Aug-1993.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜒 ↔ (𝜓 ∧ 𝜑))) → (𝜒 ↔ 𝜑)) |
|
Theorem | ccase 916 |
Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
(Proof shortened by Wolf Lammen, 6-Jan-2013.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜏)
& ⊢ ((𝜒 ∧ 𝜓) → 𝜏)
& ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
& ⊢ ((𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) |
|
Theorem | ccased 917 |
Deduction for combining cases. (Contributed by NM, 9-May-2004.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂)) & ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂)) |
|
Theorem | ccase2 918 |
Inference for combining cases. (Contributed by NM, 29-Jul-1999.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜏)
& ⊢ (𝜒 → 𝜏)
& ⊢ (𝜃 → 𝜏) ⇒ ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) |
|
Theorem | niabn 919 |
Miscellaneous inference relating falsehoods. (Contributed by NM,
31-Mar-1994.)
|
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → ((𝜒 ∧ 𝜓) ↔ ¬ 𝜑)) |
|
Theorem | dedlem0a 920 |
Alternate version of dedlema 921. (Contributed by NM, 2-Apr-1994.) (Proof
shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen,
4-Dec-2012.)
|
⊢ (𝜑 → (𝜓 ↔ ((𝜒 → 𝜑) → (𝜓 ∧ 𝜑)))) |
|
Theorem | dedlema 921 |
Lemma for iftrue 3426. (Contributed by NM, 26-Jun-2002.) (Proof
shortened
by Andrew Salmon, 7-May-2011.)
|
⊢ (𝜑 → (𝜓 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) |
|
Theorem | dedlemb 922 |
Lemma for iffalse 3429. (Contributed by NM, 15-May-1999.) (Proof
shortened
by Andrew Salmon, 7-May-2011.)
|
⊢ (¬ 𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) |
|
Theorem | pm4.42r 923 |
One direction of Theorem *4.42 of [WhiteheadRussell] p. 119. (Contributed
by Jim Kingdon, 4-Aug-2018.)
|
⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ ¬ 𝜓)) → 𝜑) |
|
Theorem | ninba 924 |
Miscellaneous inference relating falsehoods. (Contributed by NM,
31-Mar-1994.)
|
⊢ 𝜑 ⇒ ⊢ (¬ 𝜓 → (¬ 𝜑 ↔ (𝜒 ∧ 𝜓))) |
|
Theorem | prlem1 925 |
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 926 |
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 927 |
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 928 |
Lemma used in construction of real numbers. (Contributed by NM,
4-Sep-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ (((𝜑 ∧ 𝜒) ∧ (𝜓 ∧ 𝜃)) ∧ ((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜒)))) |
|
1.2.12 Abbreviated conjunction and disjunction of
three wff's
|
|
Syntax | w3o 929 |
Extend wff definition to include 3-way disjunction ('or').
|
wff (𝜑 ∨ 𝜓 ∨ 𝜒) |
|
Syntax | w3a 930 |
Extend wff definition to include 3-way conjunction ('and').
|
wff (𝜑 ∧ 𝜓 ∧ 𝜒) |
|
Definition | df-3or 931 |
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 725. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) |
|
Definition | df-3an 932 |
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 396. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
|
Theorem | 3orass 933 |
Associative law for triple disjunction. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) |
|
Theorem | 3anass 934 |
Associative law for triple conjunction. (Contributed by NM,
8-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) |
|
Theorem | 3anrot 935 |
Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) |
|
Theorem | 3orrot 936 |
Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) |
|
Theorem | 3ancoma 937 |
Commutation law for triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) |
|
Theorem | 3ancomb 938 |
Commutation law for triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) |
|
Theorem | 3orcomb 939 |
Commutation law for triple disjunction. (Contributed by Scott Fenton,
20-Apr-2011.)
|
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓)) |
|
Theorem | 3anrev 940 |
Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓 ∧ 𝜑)) |
|
Theorem | 3anan32 941 |
Convert triple conjunction to conjunction, then commute. (Contributed by
Jonathan Ben-Naim, 3-Jun-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) |
|
Theorem | 3anan12 942 |
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 943 |
Distribution of triple conjunction over conjunction. (Contributed by
David A. Wheeler, 4-Nov-2018.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) |
|
Theorem | anandi3r 944 |
Distribution of triple conjunction over conjunction. (Contributed by
David A. Wheeler, 4-Nov-2018.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓))) |
|
Theorem | 3ioran 945 |
Negated triple disjunction as triple conjunction. (Contributed by Scott
Fenton, 19-Apr-2011.)
|
⊢ (¬ (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒)) |
|
Theorem | 3simpa 946 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓)) |
|
Theorem | 3simpb 947 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒)) |
|
Theorem | 3simpc 948 |
Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)
(Proof shortened by Andrew Salmon, 13-May-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) |
|
Theorem | simp1 949 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) |
|
Theorem | simp2 950 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) |
|
Theorem | simp3 951 |
Simplification of triple conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) |
|
Theorem | simpl1 952 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) |
|
Theorem | simpl2 953 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) |
|
Theorem | simpl3 954 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) |
|
Theorem | simpr1 955 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
|
Theorem | simpr2 956 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒) |
|
Theorem | simpr3 957 |
Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃) |
|
Theorem | simp1i 958 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜑 |
|
Theorem | simp2i 959 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜓 |
|
Theorem | simp3i 960 |
Infer a conjunct from a triple conjunction. (Contributed by NM,
19-Apr-2005.)
|
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜒 |
|
Theorem | simp1d 961 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | simp2d 962 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | simp3d 963 |
Deduce a conjunct from a triple conjunction. (Contributed by NM,
4-Sep-2005.)
|
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) |
|
Theorem | simp1bi 964 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | simp2bi 965 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | simp3bi 966 |
Deduce a conjunct from a triple conjunction. (Contributed by Jonathan
Ben-Naim, 3-Jun-2011.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) |
|
Theorem | 3adant1 967 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | 3adant2 968 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒) |
|
Theorem | 3adant3 969 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Jul-1995.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) |
|
Theorem | 3ad2ant1 970 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) |
|
Theorem | 3ad2ant2 971 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒) |
|
Theorem | 3ad2ant3 972 |
Deduction adding conjuncts to an antecedent. (Contributed by NM,
21-Apr-2005.)
|
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒) |
|
Theorem | simp1l 973 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) |
|
Theorem | simp1r 974 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) |
|
Theorem | simp2l 975 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) |
|
Theorem | simp2r 976 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) |
|
Theorem | simp3l 977 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒) |
|
Theorem | simp3r 978 |
Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃) |
|
Theorem | simp11 979 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) |
|
Theorem | simp12 980 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) |
|
Theorem | simp13 981 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒) |
|
Theorem | simp21 982 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) |
|
Theorem | simp22 983 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒) |
|
Theorem | simp23 984 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜃) |
|
Theorem | simp31 985 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒) |
|
Theorem | simp32 986 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃) |
|
Theorem | simp33 987 |
Simplification of doubly triple conjunction. (Contributed by NM,
17-Nov-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏) |
|
Theorem | simpll1 988 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) |
|
Theorem | simpll2 989 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) |
|
Theorem | simpll3 990 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒) |
|
Theorem | simplr1 991 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) |
|
Theorem | simplr2 992 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓) |
|
Theorem | simplr3 993 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒) |
|
Theorem | simprl1 994 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) |
|
Theorem | simprl2 995 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) |
|
Theorem | simprl3 996 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) |
|
Theorem | simprr1 997 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
|
Theorem | simprr2 998 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) |
|
Theorem | simprr3 999 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) |
|
Theorem | simpl1l 1000 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑) |