Theorem List for Intuitionistic Logic Explorer - 201-300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 3bitr4i 201 |
A chained inference from transitive law for logical equivalence. This
inference is frequently used to apply a definition to both sides of a
logical equivalence. (Contributed by NM, 5-Aug-1993.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ (𝜒 ↔ 𝜑)
& ⊢ (𝜃 ↔ 𝜓) ⇒ ⊢ (𝜒 ↔ 𝜃) |
|
Theorem | 3bitr4ri 202 |
A chained inference from transitive law for logical equivalence.
(Contributed by NM, 2-Sep-1995.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ (𝜒 ↔ 𝜑)
& ⊢ (𝜃 ↔ 𝜓) ⇒ ⊢ (𝜃 ↔ 𝜒) |
|
Theorem | 3bitrd 203 |
Deduction from transitivity of biconditional. (Contributed by NM,
13-Aug-1999.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜏)) |
|
Theorem | 3bitrrd 204 |
Deduction from transitivity of biconditional. (Contributed by NM,
4-Aug-2006.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜒 ↔ 𝜃)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜓)) |
|
Theorem | 3bitr2d 205 |
Deduction from transitivity of biconditional. (Contributed by NM,
4-Aug-2006.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 ↔ 𝜏)) |
|
Theorem | 3bitr2rd 206 |
Deduction from transitivity of biconditional. (Contributed by NM,
4-Aug-2006.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜓)) |
|
Theorem | 3bitr3d 207 |
Deduction from transitivity of biconditional. Useful for converting
conditional definitions in a formula. (Contributed by NM,
24-Apr-1996.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 → (𝜒 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
|
Theorem | 3bitr3rd 208 |
Deduction from transitivity of biconditional. (Contributed by NM,
4-Aug-2006.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜓 ↔ 𝜃)) & ⊢ (𝜑 → (𝜒 ↔ 𝜏)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜃)) |
|
Theorem | 3bitr4d 209 |
Deduction from transitivity of biconditional. Useful for converting
conditional definitions in a formula. (Contributed by NM,
18-Oct-1995.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜓)) & ⊢ (𝜑 → (𝜏 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
|
Theorem | 3bitr4rd 210 |
Deduction from transitivity of biconditional. (Contributed by NM,
4-Aug-2006.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜓)) & ⊢ (𝜑 → (𝜏 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (𝜏 ↔ 𝜃)) |
|
Theorem | 3bitr3g 211 |
More general version of 3bitr3i 199. Useful for converting definitions
in a formula. (Contributed by NM, 4-Jun-1995.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜓 ↔ 𝜃)
& ⊢ (𝜒 ↔ 𝜏) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
|
Theorem | 3bitr4g 212 |
More general version of 3bitr4i 201. Useful for converting definitions
in a formula. (Contributed by NM, 5-Aug-1993.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 ↔ 𝜓)
& ⊢ (𝜏 ↔ 𝜒) ⇒ ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
|
Theorem | bi3ant 213 |
Construct a biconditional in antecedent position. (Contributed by Wolf
Lammen, 14-May-2013.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (((𝜃 → 𝜏) → 𝜑) → (((𝜏 → 𝜃) → 𝜓) → ((𝜃 ↔ 𝜏) → 𝜒))) |
|
Theorem | bisym 214 |
Express symmetries of theorems in terms of biconditionals. (Contributed
by Wolf Lammen, 14-May-2013.)
|
⊢ (((𝜑 → 𝜓) → (𝜒 → 𝜃)) → (((𝜓 → 𝜑) → (𝜃 → 𝜒)) → ((𝜑 ↔ 𝜓) → (𝜒 ↔ 𝜃)))) |
|
Theorem | imbi2i 215 |
Introduce an antecedent to both sides of a logical equivalence.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen,
6-Feb-2013.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓)) |
|
Theorem | bibi2i 216 |
Inference adding a biconditional to the left in an equivalence.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon,
7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ↔ 𝜑) ↔ (𝜒 ↔ 𝜓)) |
|
Theorem | bibi1i 217 |
Inference adding a biconditional to the right in an equivalence.
(Contributed by NM, 5-Aug-1993.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)) |
|
Theorem | bibi12i 218 |
The equivalence of two equivalences. (Contributed by NM,
5-Aug-1993.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜃)) |
|
Theorem | imbi2d 219 |
Deduction adding an antecedent to both sides of a logical equivalence.
(Contributed by NM, 5-Aug-1993.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 → 𝜓) ↔ (𝜃 → 𝜒))) |
|
Theorem | imbi1d 220 |
Deduction adding a consequent to both sides of a logical equivalence.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen,
17-Sep-2013.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃))) |
|
Theorem | bibi2d 221 |
Deduction adding a biconditional to the left in an equivalence.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen,
19-May-2013.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒))) |
|
Theorem | bibi1d 222 |
Deduction adding a biconditional to the right in an equivalence.
(Contributed by NM, 5-Aug-1993.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃))) |
|
Theorem | imbi12d 223 |
Deduction joining two equivalences to form equivalence of implications.
(Contributed by NM, 5-Aug-1993.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜏))) |
|
Theorem | bibi12d 224 |
Deduction joining two equivalences to form equivalence of
biconditionals. (Contributed by NM, 5-Aug-1993.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜏))) |
|
Theorem | imbi1 225 |
Theorem *4.84 of [WhiteheadRussell] p.
122. (Contributed by NM,
3-Jan-2005.)
|
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒))) |
|
Theorem | imbi2 226 |
Theorem *4.85 of [WhiteheadRussell] p.
122. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.)
|
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 → 𝜑) ↔ (𝜒 → 𝜓))) |
|
Theorem | imbi1i 227 |
Introduce a consequent to both sides of a logical equivalence.
(Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen,
17-Sep-2013.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜒)) |
|
Theorem | imbi12i 228 |
Join two logical equivalences to form equivalence of implications.
(Contributed by NM, 5-Aug-1993.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ (𝜒 ↔ 𝜃) ⇒ ⊢ ((𝜑 → 𝜒) ↔ (𝜓 → 𝜃)) |
|
Theorem | bibi1 229 |
Theorem *4.86 of [WhiteheadRussell] p.
122. (Contributed by NM,
3-Jan-2005.)
|
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))) |
|
Theorem | biimt 230 |
A wff is equivalent to itself with true antecedent. (Contributed by NM,
28-Jan-1996.)
|
⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓))) |
|
Theorem | pm5.5 231 |
Theorem *5.5 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.)
|
⊢ (𝜑 → ((𝜑 → 𝜓) ↔ 𝜓)) |
|
Theorem | a1bi 232 |
Inference rule introducing a theorem as an antecedent. (Contributed by
NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
|
⊢ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜑 → 𝜓)) |
|
Theorem | pm5.501 233 |
Theorem *5.501 of [WhiteheadRussell]
p. 125. (Contributed by NM,
3-Jan-2005.) (Revised by NM, 24-Jan-2013.)
|
⊢ (𝜑 → (𝜓 ↔ (𝜑 ↔ 𝜓))) |
|
Theorem | ibib 234 |
Implication in terms of implication and biconditional. (Contributed by
NM, 31-Mar-1994.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)
|
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜑 ↔ 𝜓))) |
|
Theorem | ibibr 235 |
Implication in terms of implication and biconditional. (Contributed by
NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 21-Dec-2013.)
|
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜓 ↔ 𝜑))) |
|
Theorem | tbt 236 |
A wff is equivalent to its equivalence with truth. (Contributed by NM,
18-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|
⊢ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜓 ↔ 𝜑)) |
|
Theorem | bi2.04 237 |
Logical equivalence of commuted antecedents. Part of Theorem *4.87 of
[WhiteheadRussell] p. 122.
(Contributed by NM, 5-Aug-1993.)
|
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜓 → (𝜑 → 𝜒))) |
|
Theorem | pm5.4 238 |
Antecedent absorption implication. Theorem *5.4 of [WhiteheadRussell]
p. 125. (Contributed by NM, 5-Aug-1993.)
|
⊢ ((𝜑 → (𝜑 → 𝜓)) ↔ (𝜑 → 𝜓)) |
|
Theorem | imdi 239 |
Distributive law for implication. Compare Theorem *5.41 of
[WhiteheadRussell] p. 125.
(Contributed by NM, 5-Aug-1993.)
|
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ ((𝜑 → 𝜓) → (𝜑 → 𝜒))) |
|
Theorem | pm5.41 240 |
Theorem *5.41 of [WhiteheadRussell] p.
125. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 12-Oct-2012.)
|
⊢ (((𝜑 → 𝜓) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 → 𝜒))) |
|
Theorem | imim21b 241 |
Simplify an implication between two implications when the antecedent of
the first is a consequence of the antecedent of the second. The reverse
form is useful in producing the successor step in induction proofs.
(Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Wolf
Lammen, 14-Sep-2013.)
|
⊢ ((𝜓 → 𝜑) → (((𝜑 → 𝜒) → (𝜓 → 𝜃)) ↔ (𝜓 → (𝜒 → 𝜃)))) |
|
Theorem | impd 242 |
Importation deduction. (Contributed by NM, 31-Mar-1994.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
|
Theorem | imp31 243 |
An importation inference. (Contributed by NM, 26-Apr-1994.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
|
Theorem | imp32 244 |
An importation inference. (Contributed by NM, 26-Apr-1994.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
|
Theorem | expd 245 |
Exportation deduction. (Contributed by NM, 20-Aug-1993.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
|
Theorem | expdimp 246 |
A deduction version of exportation, followed by importation.
(Contributed by NM, 6-Sep-2008.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
|
Theorem | impancom 247 |
Mixed importation/commutation inference. (Contributed by NM,
22-Jun-2013.)
|
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜒) → (𝜓 → 𝜃)) |
|
Theorem | pm3.3 248 |
Theorem *3.3 (Exp) of [WhiteheadRussell] p. 112. (Contributed
by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
|
⊢ (((𝜑 ∧ 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) |
|
Theorem | pm3.31 249 |
Theorem *3.31 (Imp) of [WhiteheadRussell] p. 112. (Contributed
by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
|
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 ∧ 𝜓) → 𝜒)) |
|
Theorem | impexp 250 |
Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell]
p. 122. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf
Lammen, 24-Mar-2013.)
|
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) |
|
Theorem | pm3.21 251 |
Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell]
p. 111. (Contributed by NM, 5-Aug-1993.)
|
⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜑))) |
|
Theorem | pm3.22 252 |
Theorem *3.22 of [WhiteheadRussell] p.
111. (Contributed by NM,
3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
|
⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜑)) |
|
Theorem | ancom 253 |
Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell]
p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf
Lammen, 4-Nov-2012.)
|
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) |
|
Theorem | ancomd 254 |
Commutation of conjuncts in consequent. (Contributed by Jeff Hankins,
14-Aug-2009.)
|
⊢ (𝜑 → (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → (𝜒 ∧ 𝜓)) |
|
Theorem | ancoms 255 |
Inference commuting conjunction in antecedent. (Contributed by NM,
21-Apr-1994.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
|
Theorem | ancomsd 256 |
Deduction commuting conjunction in antecedent. (Contributed by NM,
12-Dec-2004.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ (𝜑 → ((𝜒 ∧ 𝜓) → 𝜃)) |
|
Theorem | pm3.2i 257 |
Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.)
|
⊢ 𝜑
& ⊢ 𝜓 ⇒ ⊢ (𝜑 ∧ 𝜓) |
|
Theorem | pm3.43i 258 |
Nested conjunction of antecedents. (Contributed by NM, 5-Aug-1993.)
|
⊢ ((𝜑 → 𝜓) → ((𝜑 → 𝜒) → (𝜑 → (𝜓 ∧ 𝜒)))) |
|
Theorem | simplbi 259 |
Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | simprbi 260 |
Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | adantr 261 |
Inference adding a conjunct to the right of an antecedent. (Contributed
by NM, 30-Aug-1993.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜓) |
|
Theorem | adantl 262 |
Inference adding a conjunct to the left of an antecedent. (Contributed
by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑) → 𝜓) |
|
Theorem | adantld 263 |
Deduction adding a conjunct to the left of an antecedent. (Contributed
by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜒)) |
|
Theorem | adantrd 264 |
Deduction adding a conjunct to the right of an antecedent. (Contributed
by NM, 4-May-1994.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜒)) |
|
Theorem | mpan9 265 |
Modus ponens conjoining dissimilar antecedents. (Contributed by NM,
1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜒 → (𝜓 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
|
Theorem | syldan 266 |
A syllogism deduction with conjoined antecents. (Contributed by NM,
24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒)
& ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜃) |
|
Theorem | sylan 267 |
A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof
shortened by Wolf Lammen, 22-Nov-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
|
Theorem | sylanb 268 |
A syllogism inference. (Contributed by NM, 18-May-1994.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
|
Theorem | sylanbr 269 |
A syllogism inference. (Contributed by NM, 18-May-1994.)
|
⊢ (𝜓 ↔ 𝜑)
& ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜃) |
|
Theorem | sylan2 270 |
A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof
shortened by Wolf Lammen, 22-Nov-2012.)
|
⊢ (𝜑 → 𝜒)
& ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜃) |
|
Theorem | sylan2b 271 |
A syllogism inference. (Contributed by NM, 21-Apr-1994.)
|
⊢ (𝜑 ↔ 𝜒)
& ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜃) |
|
Theorem | sylan2br 272 |
A syllogism inference. (Contributed by NM, 21-Apr-1994.)
|
⊢ (𝜒 ↔ 𝜑)
& ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜃) |
|
Theorem | syl2an 273 |
A double syllogism inference. (Contributed by NM, 31-Jan-1997.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜏 → 𝜒)
& ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
|
Theorem | syl2anr 274 |
A double syllogism inference. (Contributed by NM, 17-Sep-2013.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜏 → 𝜒)
& ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜏 ∧ 𝜑) → 𝜃) |
|
Theorem | syl2anb 275 |
A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ (𝜏 ↔ 𝜒)
& ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
|
Theorem | syl2anbr 276 |
A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
|
⊢ (𝜓 ↔ 𝜑)
& ⊢ (𝜒 ↔ 𝜏)
& ⊢ ((𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜏) → 𝜃) |
|
Theorem | syland 277 |
A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜏)) |
|
Theorem | sylan2d 278 |
A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜏)) ⇒ ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → 𝜏)) |
|
Theorem | syl2and 279 |
A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜏)) & ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → 𝜂)) |
|
Theorem | biimpa 280 |
Inference from a logical equivalence. (Contributed by NM,
3-May-1994.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | biimpar 281 |
Inference from a logical equivalence. (Contributed by NM,
3-May-1994.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜒) → 𝜓) |
|
Theorem | biimpac 282 |
Inference from a logical equivalence. (Contributed by NM,
3-May-1994.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
|
Theorem | biimparc 283 |
Inference from a logical equivalence. (Contributed by NM,
3-May-1994.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜒 ∧ 𝜑) → 𝜓) |
|
Theorem | iba 284 |
Introduction of antecedent as conjunct. Theorem *4.73 of
[WhiteheadRussell] p. 121.
(Contributed by NM, 30-Mar-1994.) (Revised by
NM, 24-Mar-2013.)
|
⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) |
|
Theorem | ibar 285 |
Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.)
(Revised by NM, 24-Mar-2013.)
|
⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) |
|
Theorem | biantru 286 |
A wff is equivalent to its conjunction with truth. (Contributed by NM,
5-Aug-1993.)
|
⊢ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑)) |
|
Theorem | biantrur 287 |
A wff is equivalent to its conjunction with truth. (Contributed by NM,
3-Aug-1994.)
|
⊢ 𝜑 ⇒ ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓)) |
|
Theorem | biantrud 288 |
A wff is equivalent to its conjunction with truth. (Contributed by NM,
2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓))) |
|
Theorem | biantrurd 289 |
A wff is equivalent to its conjunction with truth. (Contributed by NM,
1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒))) |
|
Theorem | jca 290 |
Deduce conjunction of the consequents of two implications ("join
consequents with 'and'"). (Contributed by NM, 5-Aug-1993.) (Proof
shortened by Wolf Lammen, 25-Oct-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
|
Theorem | jcad 291 |
Deduction conjoining the consequents of two implications. (Contributed
by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
|
Theorem | jca31 292 |
Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃)) |
|
Theorem | jca32 293 |
Join three consequents. (Contributed by FL, 1-Aug-2009.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃))) |
|
Theorem | jcai 294 |
Deduction replacing implication with conjunction. (Contributed by NM,
5-Aug-1993.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
|
Theorem | jctil 295 |
Inference conjoining a theorem to left of consequent in an implication.
(Contributed by NM, 31-Dec-1993.)
|
⊢ (𝜑 → 𝜓)
& ⊢ 𝜒 ⇒ ⊢ (𝜑 → (𝜒 ∧ 𝜓)) |
|
Theorem | jctir 296 |
Inference conjoining a theorem to right of consequent in an implication.
(Contributed by NM, 31-Dec-1993.)
|
⊢ (𝜑 → 𝜓)
& ⊢ 𝜒 ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
|
Theorem | jctl 297 |
Inference conjoining a theorem to the left of a consequent.
(Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen,
24-Oct-2012.)
|
⊢ 𝜓 ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜑)) |
|
Theorem | jctr 298 |
Inference conjoining a theorem to the right of a consequent.
(Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen,
24-Oct-2012.)
|
⊢ 𝜓 ⇒ ⊢ (𝜑 → (𝜑 ∧ 𝜓)) |
|
Theorem | jctild 299 |
Deduction conjoining a theorem to left of consequent in an implication.
(Contributed by NM, 21-Apr-2005.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒))) |
|
Theorem | jctird 300 |
Deduction conjoining a theorem to right of consequent in an implication.
(Contributed by NM, 21-Apr-2005.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |