Theorem List for Intuitionistic Logic Explorer - 1101-1200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 3impia 1101 |
Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3impib 1102 |
Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3exp 1103 |
Exportation inference. (Contributed by NM, 30-May-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
|
Theorem | 3expa 1104 |
Exportation from triple to double conjunction. (Contributed by NM,
20-Aug-1995.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
|
Theorem | 3expb 1105 |
Exportation from triple to double conjunction. (Contributed by NM,
20-Aug-1995.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3expia 1106 |
Exportation from triple conjunction. (Contributed by NM,
19-May-2007.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
|
Theorem | 3expib 1107 |
Exportation from triple conjunction. (Contributed by NM,
19-May-2007.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
|
Theorem | 3com12 1108 |
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
|
Theorem | 3com13 1109 |
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28-Jan-1996.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) |
|
Theorem | 3com23 1110 |
Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM,
28-Jan-1996.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
|
Theorem | 3coml 1111 |
Commutation in antecedent. Rotate left. (Contributed by NM,
28-Jan-1996.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
|
Theorem | 3comr 1112 |
Commutation in antecedent. Rotate right. (Contributed by NM,
28-Jan-1996.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
|
Theorem | 3adant3r1 1113 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3adant3r2 1114 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
17-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3adant3r3 1115 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
18-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) |
|
Theorem | 3an1rs 1116 |
Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒) → 𝜏) |
|
Theorem | 3imp1 1117 |
Importation to left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
|
Theorem | 3impd 1118 |
Importation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
|
Theorem | 3imp2 1119 |
Importation to right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) |
|
Theorem | 3exp1 1120 |
Exportation from left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
|
Theorem | 3expd 1121 |
Exportation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
|
Theorem | 3exp2 1122 |
Exportation from right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
|
Theorem | exp5o 1123 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) |
|
Theorem | exp516 1124 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) |
|
Theorem | exp520 1125 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) |
|
Theorem | 3anassrs 1126 |
Associative law for conjunction applied to antecedent (eliminates
syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) |
|
Theorem | 3adant1l 1127 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3adant1r 1128 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3adant2l 1129 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
|
Theorem | 3adant2r 1130 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
|
Theorem | 3adant3l 1131 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3adant3r 1132 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) |
|
Theorem | syl12anc 1133 |
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1-Aug-2009.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (𝜑 → 𝜏) |
|
Theorem | syl21anc 1134 |
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1-Aug-2009.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → 𝜏) |
|
Theorem | syl3anc 1135 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → 𝜏) |
|
Theorem | syl22anc 1136 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl13anc 1137 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl31anc 1138 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl112anc 1139 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl121anc 1140 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl211anc 1141 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl23anc 1142 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl32anc 1143 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl122anc 1144 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl212anc 1145 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl221anc 1146 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl113anc 1147 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl131anc 1148 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl311anc 1149 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl33anc 1150 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl222anc 1151 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl123anc 1152 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl132anc 1153 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl213anc 1154 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl231anc 1155 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl312anc 1156 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl321anc 1157 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl133anc 1158 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl313anc 1159 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl331anc 1160 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl223anc 1161 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl232anc 1162 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl322anc 1163 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl233anc 1164 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (𝜑 → 𝜌)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) |
|
Theorem | syl323anc 1165 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (𝜑 → 𝜌)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) |
|
Theorem | syl332anc 1166 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (𝜑 → 𝜌)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) |
|
Theorem | syl333anc 1167 |
A syllogism inference combined with contraction. (Contributed by NM,
10-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (𝜑 → 𝜌)
& ⊢ (𝜑 → 𝜇)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌 ∧ 𝜇)) → 𝜆) ⇒ ⊢ (𝜑 → 𝜆) |
|
Theorem | syl3an1 1168 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜑 → 𝜓)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3an2 1169 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜑 → 𝜒)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3an3 1170 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜑 → 𝜃)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
|
Theorem | syl3an1b 1171 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3an2b 1172 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜑 ↔ 𝜒)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3an3b 1173 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜑 ↔ 𝜃)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
|
Theorem | syl3an1br 1174 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜓 ↔ 𝜑)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3an2br 1175 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜒 ↔ 𝜑)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3an3br 1176 |
A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|
⊢ (𝜃 ↔ 𝜑)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) |
|
Theorem | syl3an 1177 |
A triple syllogism inference. (Contributed by NM, 13-May-2004.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜒 → 𝜃)
& ⊢ (𝜏 → 𝜂)
& ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) |
|
Theorem | syl3anb 1178 |
A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ (𝜒 ↔ 𝜃)
& ⊢ (𝜏 ↔ 𝜂)
& ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) |
|
Theorem | syl3anbr 1179 |
A triple syllogism inference. (Contributed by NM, 29-Dec-2011.)
|
⊢ (𝜓 ↔ 𝜑)
& ⊢ (𝜃 ↔ 𝜒)
& ⊢ (𝜂 ↔ 𝜏)
& ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) |
|
Theorem | syld3an3 1180 |
A syllogism inference. (Contributed by NM, 20-May-2007.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
& ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜏) |
|
Theorem | syld3an1 1181 |
A syllogism inference. (Contributed by NM, 7-Jul-2008.)
|
⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑)
& ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏) |
|
Theorem | syld3an2 1182 |
A syllogism inference. (Contributed by NM, 20-May-2007.)
|
⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜓)
& ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) |
|
Theorem | syl3anl1 1183 |
A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) |
|
Theorem | syl3anl2 1184 |
A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|
⊢ (𝜑 → 𝜒)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜃) ∧ 𝜏) → 𝜂) |
|
Theorem | syl3anl3 1185 |
A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|
⊢ (𝜑 → 𝜃)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜑) ∧ 𝜏) → 𝜂) |
|
Theorem | syl3anl 1186 |
A triple syllogism inference. (Contributed by NM, 24-Dec-2006.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜒 → 𝜃)
& ⊢ (𝜏 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜃 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (((𝜑 ∧ 𝜒 ∧ 𝜏) ∧ 𝜁) → 𝜎) |
|
Theorem | syl3anr1 1187 |
A syllogism inference. (Contributed by NM, 31-Jul-2007.)
|
⊢ (𝜑 → 𝜓)
& ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃 ∧ 𝜏)) → 𝜂) |
|
Theorem | syl3anr2 1188 |
A syllogism inference. (Contributed by NM, 1-Aug-2007.)
|
⊢ (𝜑 → 𝜃)
& ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜑 ∧ 𝜏)) → 𝜂) |
|
Theorem | syl3anr3 1189 |
A syllogism inference. (Contributed by NM, 23-Aug-2007.)
|
⊢ (𝜑 → 𝜏)
& ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ ((𝜒 ∧ (𝜓 ∧ 𝜃 ∧ 𝜑)) → 𝜂) |
|
Theorem | 3impdi 1190 |
Importation inference (undistribute conjunction). (Contributed by NM,
14-Aug-1995.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3impdir 1191 |
Importation inference (undistribute conjunction). (Contributed by NM,
20-Aug-1995.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜓)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
|
Theorem | 3anidm12 1192 |
Inference from idempotent law for conjunction. (Contributed by NM,
7-Mar-2008.)
|
⊢ ((𝜑 ∧ 𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | 3anidm13 1193 |
Inference from idempotent law for conjunction. (Contributed by NM,
7-Mar-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | 3anidm23 1194 |
Inference from idempotent law for conjunction. (Contributed by NM,
1-Feb-2007.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | 3ori 1195 |
Infer implication from triple disjunction. (Contributed by NM,
26-Sep-2006.)
|
⊢ (𝜑 ∨ 𝜓 ∨ 𝜒) ⇒ ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → 𝜒) |
|
Theorem | 3jao 1196 |
Disjunction of 3 antecedents. (Contributed by NM, 8-Apr-1994.)
|
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)) |
|
Theorem | 3jaob 1197 |
Disjunction of 3 antecedents. (Contributed by NM, 13-Sep-2011.)
|
⊢ (((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))) |
|
Theorem | 3jaoi 1198 |
Disjunction of 3 antecedents (inference). (Contributed by NM,
12-Sep-1995.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜒 → 𝜓)
& ⊢ (𝜃 → 𝜓) ⇒ ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓) |
|
Theorem | 3jaod 1199 |
Disjunction of 3 antecedents (deduction). (Contributed by NM,
14-Oct-2005.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜃 → 𝜒)) & ⊢ (𝜑 → (𝜏 → 𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 ∨ 𝜃 ∨ 𝜏) → 𝜒)) |
|
Theorem | 3jaoian 1200 |
Disjunction of 3 antecedents (inference). (Contributed by NM,
14-Oct-2005.)
|
⊢ ((𝜑 ∧ 𝜓) → 𝜒)
& ⊢ ((𝜃 ∧ 𝜓) → 𝜒)
& ⊢ ((𝜏 ∧ 𝜓) → 𝜒) ⇒ ⊢ (((𝜑 ∨ 𝜃 ∨ 𝜏) ∧ 𝜓) → 𝜒) |