Theorem List for Intuitionistic Logic Explorer - 1201-1300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 3adant3r1 1201 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3adant3r2 1202 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
17-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3adant3r3 1203 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
18-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) |
|
Theorem | ad4ant123 1204 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜃) |
|
Theorem | ad4ant124 1205 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃) |
|
Theorem | ad4ant134 1206 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃) |
|
Theorem | ad4ant234 1207 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃) |
|
Theorem | 3an1rs 1208 |
Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒) → 𝜏) |
|
Theorem | 3imp1 1209 |
Importation to left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
|
Theorem | 3impd 1210 |
Importation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
|
Theorem | 3imp2 1211 |
Importation to right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) |
|
Theorem | 3exp1 1212 |
Exportation from left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
|
Theorem | 3expd 1213 |
Exportation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
|
Theorem | 3exp2 1214 |
Exportation from right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
|
Theorem | exp5o 1215 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) |
|
Theorem | exp516 1216 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) |
|
Theorem | exp520 1217 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) |
|
Theorem | 3anassrs 1218 |
Associative law for conjunction applied to antecedent (eliminates
syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) |
|
Theorem | 3adant1l 1219 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3adant1r 1220 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3adant2l 1221 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
|
Theorem | 3adant2r 1222 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
|
Theorem | 3adant3l 1223 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3adant3r 1224 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) |
|
Theorem | syl12anc 1225 |
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1-Aug-2009.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (𝜑 → 𝜏) |
|
Theorem | syl21anc 1226 |
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1-Aug-2009.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → 𝜏) |
|
Theorem | syl3anc 1227 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → 𝜏) |
|
Theorem | syl22anc 1228 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl13anc 1229 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl31anc 1230 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl112anc 1231 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl121anc 1232 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl211anc 1233 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl23anc 1234 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl32anc 1235 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl122anc 1236 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl212anc 1237 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl221anc 1238 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl113anc 1239 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl131anc 1240 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl311anc 1241 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl33anc 1242 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl222anc 1243 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl123anc 1244 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl132anc 1245 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl213anc 1246 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl231anc 1247 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl312anc 1248 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl321anc 1249 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl133anc 1250 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl313anc 1251 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl331anc 1252 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl223anc 1253 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl232anc 1254 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl322anc 1255 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl233anc 1256 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (𝜑 → 𝜌)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) |
|
Theorem | syl323anc 1257 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (𝜑 → 𝜌)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) |
|
Theorem | syl332anc 1258 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (𝜑 → 𝜌)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) |
|
Theorem | syl333anc 1259 |
A syllogism inference combined with contraction. (Contributed by NM,
10-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (𝜑 → 𝜌)
& ⊢ (𝜑 → 𝜇)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌 ∧ 𝜇)) → 𝜆) ⇒ ⊢ (𝜑 → 𝜆) |
|
Theorem | syl3an1 1260 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜑 → 𝜓)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3an2 1261 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜑 → 𝜒)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3an3 1262 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜑 → 𝜃)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
|
Theorem | syl3an1b 1263 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3an2b 1264 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜑 ↔ 𝜒)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3an3b 1265 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜑 ↔ 𝜃)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
|
Theorem | syl3an1br 1266 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜓 ↔ 𝜑)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3an2br 1267 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜒 ↔ 𝜑)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3an3br 1268 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜃 ↔ 𝜑)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
|
Theorem | syl3an 1269 |
A triple syllogism inference. (Contributed by NM, 13-May-2004.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜒 → 𝜃)
& ⊢ (𝜏 → 𝜂)
& ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) |
|
Theorem | syl3anb 1270 |
A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ (𝜒 ↔ 𝜃)
& ⊢ (𝜏 ↔ 𝜂)
& ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) |
|
Theorem | syl3anbr 1271 |
A triple syllogism inference. (Contributed by NM, 29-Dec-2011.)
|
⊢ (𝜓 ↔ 𝜑)
& ⊢ (𝜃 ↔ 𝜒)
& ⊢ (𝜂 ↔ 𝜏)
& ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) |
|
Theorem | syld3an3 1272 |
A syllogism inference. (Contributed by NM, 20-May-2007.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
& ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
|
Theorem | syld3an1 1273 |
A syllogism inference. (Contributed by NM, 7-Jul-2008.)
|
⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑)
& ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
|
Theorem | syld3an2 1274 |
A syllogism inference. (Contributed by NM, 20-May-2007.)
|
⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)
& ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3anl1 1275 |
A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) |
|
Theorem | syl3anl2 1276 |
A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|
⊢ (𝜑 → 𝜒)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜃) ∧ 𝜏) → 𝜂) |
|
Theorem | syl3anl3 1277 |
A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|
⊢ (𝜑 → 𝜃)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜑) ∧ 𝜏) → 𝜂) |
|
Theorem | syl3anl 1278 |
A triple syllogism inference. (Contributed by NM, 24-Dec-2006.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜒 → 𝜃)
& ⊢ (𝜏 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜃 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ 𝜁) → 𝜎) |
|
Theorem | syl3anr1 1279 |
A syllogism inference. (Contributed by NM, 31-Jul-2007.)
|
⊢ (𝜑 → 𝜓)
& ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃 ∧ 𝜏)) → 𝜂) |
|
Theorem | syl3anr2 1280 |
A syllogism inference. (Contributed by NM, 1-Aug-2007.)
|
⊢ (𝜑 → 𝜃)
& ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑 ∧ 𝜏)) → 𝜂) |
|
Theorem | syl3anr3 1281 |
A syllogism inference. (Contributed by NM, 23-Aug-2007.)
|
⊢ (𝜑 → 𝜏)
& ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜑)) → 𝜂) |
|
Theorem | 3impdi 1282 |
Importation inference (undistribute conjunction). (Contributed by NM,
14-Aug-1995.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3impdir 1283 |
Importation inference (undistribute conjunction). (Contributed by NM,
20-Aug-1995.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
|
Theorem | 3anidm12 1284 |
Inference from idempotent law for conjunction. (Contributed by NM,
7-Mar-2008.)
|
⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | 3anidm13 1285 |
Inference from idempotent law for conjunction. (Contributed by NM,
7-Mar-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | 3anidm23 1286 |
Inference from idempotent law for conjunction. (Contributed by NM,
1-Feb-2007.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | syl2an3an 1287 |
syl3an 1269 with antecedents in standard conjunction
form. (Contributed by
Alan Sare, 31-Aug-2016.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜃 → 𝜏)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜃) → 𝜂) |
|
Theorem | syl2an23an 1288 |
Deduction related to syl3an 1269 with antecedents in standard conjunction
form. (Contributed by Alan Sare, 31-Aug-2016.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ ((𝜃 ∧ 𝜑) → 𝜏)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ((𝜃 ∧ 𝜑) → 𝜂) |
|
Theorem | 3ori 1289 |
Infer implication from triple disjunction. (Contributed by NM,
26-Sep-2006.)
|
⊢ (𝜑 ∨ 𝜓 ∨ 𝜒) ⇒ ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒) |
|
Theorem | 3jao 1290 |
Disjunction of 3 antecedents. (Contributed by NM, 8-Apr-1994.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)) |
|
Theorem | 3jaob 1291 |
Disjunction of 3 antecedents. (Contributed by NM, 13-Sep-2011.)
|
⊢ (((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))) |
|
Theorem | 3jaoi 1292 |
Disjunction of 3 antecedents (inference). (Contributed by NM,
12-Sep-1995.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜒 → 𝜓)
& ⊢ (𝜃 → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) |
|
Theorem | 3jaod 1293 |
Disjunction of 3 antecedents (deduction). (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜒)) & ⊢ (𝜑 → (𝜏 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) |
|
Theorem | 3jaoian 1294 |
Disjunction of 3 antecedents (inference). (Contributed by NM,
14-Oct-2005.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒)
& ⊢ ((𝜃 ∧ 𝜓) → 𝜒)
& ⊢ ((𝜏 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜑 ∨ 𝜃 ∨ 𝜏) ∧ 𝜓) → 𝜒) |
|
Theorem | 3jaodan 1295 |
Disjunction of 3 antecedents (deduction). (Contributed by NM,
14-Oct-2005.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒)
& ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
& ⊢ ((𝜑 ∧ 𝜏) → 𝜒) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃 ∨ 𝜏)) → 𝜒) |
|
Theorem | mpjao3dan 1296 |
Eliminate a 3-way disjunction in a deduction. (Contributed by Thierry
Arnoux, 13-Apr-2018.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒)
& ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
& ⊢ ((𝜑 ∧ 𝜏) → 𝜒)
& ⊢ (𝜑 → (𝜓 ∨ 𝜃 ∨ 𝜏)) ⇒ ⊢ (𝜑 → 𝜒) |
|
Theorem | 3jaao 1297 |
Inference conjoining and disjoining the antecedents of three
implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof
shortened by Andrew Salmon, 13-May-2011.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜃 → (𝜏 → 𝜒)) & ⊢ (𝜂 → (𝜁 → 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜂) → ((𝜓 ∨ 𝜏 ∨ 𝜁) → 𝜒)) |
|
Theorem | 3ianorr 1298 |
Triple disjunction implies negated triple conjunction. (Contributed by
Jim Kingdon, 23-Dec-2018.)
|
⊢ ((¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒) → ¬ (𝜑 ∧ 𝜓 ∧ 𝜒)) |
|
Theorem | syl3an9b 1299 |
Nested syllogism inference conjoining 3 dissimilar antecedents.
(Contributed by NM, 1-May-1995.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜃 → (𝜒 ↔ 𝜏)) & ⊢ (𝜂 → (𝜏 ↔ 𝜁)) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜂) → (𝜓 ↔ 𝜁)) |
|
Theorem | 3orbi123d 1300 |
Deduction joining 3 equivalences to form equivalence of disjunctions.
(Contributed by NM, 20-Apr-1994.)
|
⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → (𝜃 ↔ 𝜏)) & ⊢ (𝜑 → (𝜂 ↔ 𝜁)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜂) ↔ (𝜒 ∨ 𝜏 ∨ 𝜁))) |