Home | Metamath
Proof Explorer Theorem List (p. 11 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bianir 1001 | If a wff is equivalent to its conjunction with another wff, the other wwf follows. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Roger Witte, 17-Aug-2020.) |
⊢ ((𝜑 ∧ (𝜓 ↔ 𝜑)) → 𝜓) | ||
Theorem | jaoi2 1002 | Inference removing a negated conjunct in a disjunction of an antecedent if this conjunct is part of the disjunction. (Contributed by Alexander van der Vekens, 3-Nov-2017.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) |
⊢ ((𝜑 ∨ (¬ 𝜑 ∧ 𝜒)) → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒) → 𝜓) | ||
Theorem | jaoi3 1003 | Inference separating a disjunct of an antecedent. (Contributed by Alexander van der Vekens, 25-May-2018.) |
⊢ (𝜑 → 𝜓) & ⊢ ((¬ 𝜑 ∧ 𝜒) → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒) → 𝜓) | ||
Theorem | cases 1004 | Case disjunction according to the value of 𝜑. (Contributed by NM, 25-Apr-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (¬ 𝜑 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜓 ↔ ((𝜑 ∧ 𝜒) ∨ (¬ 𝜑 ∧ 𝜃))) | ||
Theorem | cases2 1005 | Case disjunction according to the value of 𝜑. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 2-Jan-2020.) |
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) | ||
This subsection introduces the conditional operator for propositions, denoted by if- (see df-ifp 1007). It is the analogue for propositions of the conditional operator for classes if (see df-if 4037). | ||
Syntax | wif 1006 | Extend class notation to include the conditional operator for propositions. |
wff if-(𝜑, 𝜓, 𝜒) | ||
Definition | df-ifp 1007 |
Definition of the conditional operator for propositions. The value of
if-(𝜑,
𝜓, 𝜒) is 𝜓 if 𝜑 is true and 𝜒 if 𝜑
false. See dfifp2 1008, dfifp3 1009, dfifp4 1010, dfifp5 1011, dfifp6 1012 and
dfifp7 1013 for alternate definitions.
This definition (in the form of dfifp2 1008) appears in Section II.24 of [Church] p. 129 (Definition D12 page 132), where it is called "conditioned disjunction". Church's [𝜓, 𝜑, 𝜒] corresponds to our if-(𝜑, 𝜓, 𝜒) (note the permutation of the first two variables). Church uses the conditional operator as an intermediate step to prove completeness of some systems of connectives. The first result is that the system {if-, ⊤, ⊥} is complete: for the induction step, consider a wff with n+1 variables; single out one variable, say 𝜑; when one sets 𝜑 to True (resp. False), then what remains is a wff of n variables, so by the induction hypothesis it corresponds to a formula using only {if-, ⊤, ⊥}, say 𝜓 (resp. 𝜒); therefore, the formula if-(𝜑, 𝜓, 𝜒) represents the initial wff. Now, since { → , ¬ } and similar systems suffice to express if-, ⊤, ⊥, they are also complete. (Contributed by BJ, 22-Jun-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) | ||
Theorem | dfifp2 1008 | Alternate definition of the conditional operator for propositions. The value of if-(𝜑, 𝜓, 𝜒) is "if 𝜑 then 𝜓, and if not 𝜑 then 𝜒." This is the definition used in Section II.24 of [Church] p. 129 (Definition D12 page 132) (see comment of df-ifp 1007). (Contributed by BJ, 22-Jun-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) | ||
Theorem | dfifp3 1009 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 → 𝜓) ∧ (𝜑 ∨ 𝜒))) | ||
Theorem | dfifp4 1010 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 30-Sep-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒))) | ||
Theorem | dfifp5 1011 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (¬ 𝜑 → 𝜒))) | ||
Theorem | dfifp6 1012 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ ¬ (𝜒 → 𝜑))) | ||
Theorem | dfifp7 1013 | Alternate definition of the conditional operator for propositions. (Contributed by BJ, 2-Oct-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜒 → 𝜑) → (𝜑 ∧ 𝜓))) | ||
Theorem | anifp 1014 | The conditional operator is implied by the conjunction of its possible outputs. Dual statement of ifpor 1015. (Contributed by BJ, 30-Sep-2019.) |
⊢ ((𝜓 ∧ 𝜒) → if-(𝜑, 𝜓, 𝜒)) | ||
Theorem | ifpor 1015 | The conditional operator implies the disjunction of its possible outputs. Dual statement of anifp 1014. (Contributed by BJ, 1-Oct-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) → (𝜓 ∨ 𝜒)) | ||
Theorem | ifpn 1016 | Conditional operator for the negation of a proposition. (Contributed by BJ, 30-Sep-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜒) ↔ if-(¬ 𝜑, 𝜒, 𝜓)) | ||
Theorem | ifptru 1017 | Value of the conditional operator for propositions when its first argument is true. Analogue for propositions of iftrue 4042. This is essentially dedlema 993. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 10-Jul-2020.) |
⊢ (𝜑 → (if-(𝜑, 𝜓, 𝜒) ↔ 𝜓)) | ||
Theorem | ifpfal 1018 | Value of the conditional operator for propositions when its first argument is false. Analogue for propositions of iffalse 4045. This is essentially dedlemb 994. (Contributed by BJ, 20-Sep-2019.) (Proof shortened by Wolf Lammen, 25-Jun-2020.) |
⊢ (¬ 𝜑 → (if-(𝜑, 𝜓, 𝜒) ↔ 𝜒)) | ||
Theorem | ifpid 1019 | Value of the conditional operator for propositions when the same proposition is returned in either case. Analogue for propositions of ifid 4075. This is essentially pm4.42 995. (Contributed by BJ, 20-Sep-2019.) |
⊢ (if-(𝜑, 𝜓, 𝜓) ↔ 𝜓) | ||
Theorem | casesifp 1020 | Version of cases 1004 expressed using if-. Case disjunction according to the value of 𝜑. One can see this as a proof that the two hypotheses characterize the conditional operator for propositions. For the converses, see ifptru 1017 and ifpfal 1018. (Contributed by BJ, 20-Sep-2019.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (¬ 𝜑 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (𝜓 ↔ if-(𝜑, 𝜒, 𝜃)) | ||
Theorem | ifpbi123d 1021 | Equality deduction for conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) |
⊢ (𝜑 → (𝜓 ↔ 𝜏)) & ⊢ (𝜑 → (𝜒 ↔ 𝜂)) & ⊢ (𝜑 → (𝜃 ↔ 𝜁)) ⇒ ⊢ (𝜑 → (if-(𝜓, 𝜒, 𝜃) ↔ if-(𝜏, 𝜂, 𝜁))) | ||
Theorem | ifpimpda 1022 | Separation of the values of the conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 27-Feb-2021.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) & ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝜃) ⇒ ⊢ (𝜑 → if-(𝜓, 𝜒, 𝜃)) | ||
Theorem | 1fpid3 1023 | The value of the conditional operator for propositions is its third argument if the first and second argument imply the third argument. (Contributed by AV, 4-Apr-2021.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (if-(𝜑, 𝜓, 𝜒) → 𝜒) | ||
This subsection contains a few results related to the weak deduction theorem. For more information, see the Weak Deduction Theorem page mmdeduction.html. | ||
Theorem | elimh 1024 | Hypothesis builder for the weak deduction theorem. For more information, see the Weak Deduction Theorem page mmdeduction.html. (Contributed by NM, 26-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) |
⊢ ((if-(𝜒, 𝜑, 𝜓) ↔ 𝜑) → (𝜒 ↔ 𝜏)) & ⊢ ((if-(𝜒, 𝜑, 𝜓) ↔ 𝜓) → (𝜃 ↔ 𝜏)) & ⊢ 𝜃 ⇒ ⊢ 𝜏 | ||
Theorem | dedt 1025 | The weak deduction theorem. For more information, see the Weak Deduction Theorem page mmdeduction.html. (Contributed by NM, 26-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) |
⊢ ((if-(𝜒, 𝜑, 𝜓) ↔ 𝜑) → (𝜃 ↔ 𝜏)) & ⊢ 𝜏 ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | con3ALT 1026 | Proof of con3 148 from its associated inference con3i 149 that illustrates the use of the weak deduction theorem dedt 1025. (Contributed by NM, 27-Jun-2002.) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | ||
Theorem | elimhOLD 1027 | Old version of elimh 1024. Obsolete as of 16-Mar-2021. (Contributed by NM, 26-Jun-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) → (𝜒 ↔ 𝜏)) & ⊢ ((𝜓 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) → (𝜃 ↔ 𝜏)) & ⊢ 𝜃 ⇒ ⊢ 𝜏 | ||
Theorem | dedtOLD 1028 | Old version of dedt 1025. Obsolete as of 16-Mar-2021. (Contributed by NM, 26-Jun-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ↔ ((𝜑 ∧ 𝜒) ∨ (𝜓 ∧ ¬ 𝜒))) → (𝜃 ↔ 𝜏)) & ⊢ 𝜏 ⇒ ⊢ (𝜒 → 𝜃) | ||
Theorem | con3OLD 1029 | Old version of con3ALT 1026. Obsolete as of 16-Mar-2021. (Contributed by NM, 27-Jun-2002.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑)) | ||
Syntax | w3o 1030 | Extend wff definition to include three-way disjunction ('or'). |
wff (𝜑 ∨ 𝜓 ∨ 𝜒) | ||
Syntax | w3a 1031 | Extend wff definition to include three-way conjunction ('and'). |
wff (𝜑 ∧ 𝜓 ∧ 𝜒) | ||
Definition | df-3or 1032 | Define disjunction ('or') of three 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 545. (Contributed by NM, 8-Apr-1994.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒)) | ||
Definition | df-3an 1033 | Define conjunction ('and') of three 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 679. (Contributed by NM, 8-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) | ||
Theorem | 3orass 1034 | Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒))) | ||
Theorem | 3anass 1035 | Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒))) | ||
Theorem | 3anrot 1036 | Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑)) | ||
Theorem | 3orrot 1037 | Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑)) | ||
Theorem | 3ancoma 1038 | Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒)) | ||
Theorem | 3orcoma 1039 | Commutation law for triple disjunction. (Contributed by Mario Carneiro, 4-Sep-2016.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜑 ∨ 𝜒)) | ||
Theorem | 3ancomb 1040 | Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ 𝜒 ∧ 𝜓)) | ||
Theorem | 3orcomb 1041 | Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓)) | ||
Theorem | 3anrev 1042 | Reversal law for triple conjunction. (Contributed by NM, 21-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜒 ∧ 𝜓 ∧ 𝜑)) | ||
Theorem | 3anan32 1043 | Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜒) ∧ 𝜓)) | ||
Theorem | 3anan12 1044 | 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 1045 | Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒))) | ||
Theorem | anandi3r 1046 | Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓))) | ||
Theorem | 3anor 1047 | Triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒)) | ||
Theorem | 3ianor 1048 | Negated triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ (¬ (𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒)) | ||
Theorem | 3ioran 1049 | Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.) |
⊢ (¬ (𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒)) | ||
Theorem | 3oran 1050 | Triple disjunction in terms of triple conjunction. (Contributed by NM, 8-Oct-2012.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ¬ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒)) | ||
Theorem | 3simpa 1051 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓)) | ||
Theorem | 3simpb 1052 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒)) | ||
Theorem | 3simpc 1053 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | ||
Theorem | simp1 1054 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | ||
Theorem | simp2 1055 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | ||
Theorem | simp3 1056 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | ||
Theorem | simpl1 1057 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) | ||
Theorem | simpl2 1058 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | ||
Theorem | simpl3 1059 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) | ||
Theorem | simpr1 1060 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓) | ||
Theorem | simpr2 1061 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒) | ||
Theorem | simpr3 1062 | Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃) | ||
Theorem | simp1i 1063 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜑 | ||
Theorem | simp2i 1064 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜓 | ||
Theorem | simp3i 1065 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | simp1d 1066 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | simp2d 1067 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | simp3d 1068 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | simp1bi 1069 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | simp2bi 1070 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | simp3bi 1071 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | 3adant1 1072 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | 3adant2 1073 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒) | ||
Theorem | 3adant3 1074 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | ||
Theorem | 3ad2ant1 1075 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | ||
Theorem | 3ad2ant2 1076 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒) | ||
Theorem | 3ad2ant3 1077 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒) | ||
Theorem | simp1l 1078 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) | ||
Theorem | simp1r 1079 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | ||
Theorem | simp2l 1080 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | ||
Theorem | simp2r 1081 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) | ||
Theorem | simp3l 1082 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒) | ||
Theorem | simp3r 1083 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃) | ||
Theorem | simp11 1084 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
Theorem | simp12 1085 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
Theorem | simp13 1086 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒) | ||
Theorem | simp21 1087 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simp22 1088 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒) | ||
Theorem | simp23 1089 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜃) | ||
Theorem | simp31 1090 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜒) | ||
Theorem | simp32 1091 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜃) | ||
Theorem | simp33 1092 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜏) | ||
Theorem | simpll1 1093 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑) | ||
Theorem | simpll2 1094 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simpll3 1095 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒) | ||
Theorem | simplr1 1096 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜑) | ||
Theorem | simplr2 1097 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜓) | ||
Theorem | simplr3 1098 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏) → 𝜒) | ||
Theorem | simprl1 1099 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) | ||
Theorem | simprl2 1100 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |