Theorem List for Intuitionistic Logic Explorer - 1101-1200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | simp22r 1101 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓) |
|
Theorem | simp23l 1102 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑) |
|
Theorem | simp23r 1103 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓) |
|
Theorem | simp31l 1104 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) |
|
Theorem | simp31r 1105 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) |
|
Theorem | simp32l 1106 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) |
|
Theorem | simp32r 1107 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) |
|
Theorem | simp33l 1108 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) |
|
Theorem | simp33r 1109 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) |
|
Theorem | simp111 1110 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑) |
|
Theorem | simp112 1111 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓) |
|
Theorem | simp113 1112 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
|
Theorem | simp121 1113 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑) |
|
Theorem | simp122 1114 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓) |
|
Theorem | simp123 1115 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
|
Theorem | simp131 1116 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑) |
|
Theorem | simp132 1117 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜓) |
|
Theorem | simp133 1118 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒) |
|
Theorem | simp211 1119 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜑) |
|
Theorem | simp212 1120 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜓) |
|
Theorem | simp213 1121 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜒) |
|
Theorem | simp221 1122 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜑) |
|
Theorem | simp222 1123 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜓) |
|
Theorem | simp223 1124 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜒) |
|
Theorem | simp231 1125 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜑) |
|
Theorem | simp232 1126 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜓) |
|
Theorem | simp233 1127 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜒) |
|
Theorem | simp311 1128 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ 𝜁 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜑) |
|
Theorem | simp312 1129 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ 𝜁 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜓) |
|
Theorem | simp313 1130 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ 𝜁 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜒) |
|
Theorem | simp321 1131 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜑) |
|
Theorem | simp322 1132 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜓) |
|
Theorem | simp323 1133 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜒) |
|
Theorem | simp331 1134 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
|
Theorem | simp332 1135 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) |
|
Theorem | simp333 1136 |
Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
|
⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) |
|
Theorem | 3adantl1 1137 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
24-Feb-2005.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
|
Theorem | 3adantl2 1138 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
24-Feb-2005.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
|
Theorem | 3adantl3 1139 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
24-Feb-2005.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
|
Theorem | 3adantr1 1140 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
27-Apr-2005.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3adantr2 1141 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
27-Apr-2005.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3adantr3 1142 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
27-Apr-2005.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) |
|
Theorem | 3ad2antl1 1143 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
|
Theorem | 3ad2antl2 1144 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
|
Theorem | 3ad2antl3 1145 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃) |
|
Theorem | 3ad2antr1 1146 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
25-Dec-2007.)
|
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) |
|
Theorem | 3ad2antr2 1147 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
27-Dec-2007.)
|
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) |
|
Theorem | 3ad2antr3 1148 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
30-Dec-2007.)
|
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3anibar 1149 |
Remove a hypothesis from the second member of a biimplication.
(Contributed by FL, 22-Jul-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ (𝜒 ∧ 𝜏))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) |
|
Theorem | 3mix1 1150 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) |
|
Theorem | 3mix2 1151 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
⊢ (𝜑 → (𝜓 ∨ 𝜑 ∨ 𝜒)) |
|
Theorem | 3mix3 1152 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑)) |
|
Theorem | 3mix1i 1153 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
⊢ 𝜑 ⇒ ⊢ (𝜑 ∨ 𝜓 ∨ 𝜒) |
|
Theorem | 3mix2i 1154 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
⊢ 𝜑 ⇒ ⊢ (𝜓 ∨ 𝜑 ∨ 𝜒) |
|
Theorem | 3mix3i 1155 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
⊢ 𝜑 ⇒ ⊢ (𝜓 ∨ 𝜒 ∨ 𝜑) |
|
Theorem | 3mix1d 1156 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃)) |
|
Theorem | 3mix2d 1157 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃)) |
|
Theorem | 3mix3d 1158 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓)) |
|
Theorem | 3pm3.2i 1159 |
Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)
|
⊢ 𝜑
& ⊢ 𝜓
& ⊢ 𝜒 ⇒ ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) |
|
Theorem | pm3.2an3 1160 |
pm3.2 138 for a triple conjunction. (Contributed by
Alan Sare,
24-Oct-2011.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 ∧ 𝜓 ∧ 𝜒)))) |
|
Theorem | 3jca 1161 |
Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
|
Theorem | 3jcad 1162 |
Deduction conjoining the consequents of three implications.
(Contributed by NM, 25-Sep-2005.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏))) |
|
Theorem | mpbir3an 1163 |
Detach a conjunction of truths in a biconditional. (Contributed by NM,
16-Sep-2011.) (Revised by NM, 9-Jan-2015.)
|
⊢ 𝜓
& ⊢ 𝜒
& ⊢ 𝜃
& ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ 𝜑 |
|
Theorem | mpbir3and 1164 |
Detach a conjunction of truths in a biconditional. (Contributed by
Mario Carneiro, 11-May-2014.)
|
⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | syl3anbrc 1165 |
Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜏) |
|
Theorem | 3anim123i 1166 |
Join antecedents and consequents with conjunction. (Contributed by NM,
8-Apr-1994.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜒 → 𝜃)
& ⊢ (𝜏 → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂)) |
|
Theorem | 3anim1i 1167 |
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 16-Aug-2009.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
|
Theorem | 3anim2i 1168 |
Add two conjuncts to antecedent and consequent. (Contributed by AV,
21-Nov-2019.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜓 ∧ 𝜃)) |
|
Theorem | 3anim3i 1169 |
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 19-Aug-2009.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓)) |
|
Theorem | 3anbi123i 1170 |
Join 3 biconditionals with conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ (𝜒 ↔ 𝜃)
& ⊢ (𝜏 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) |
|
Theorem | 3orbi123i 1171 |
Join 3 biconditionals with disjunction. (Contributed by NM,
17-May-1994.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ (𝜒 ↔ 𝜃)
& ⊢ (𝜏 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)) |
|
Theorem | 3anbi1i 1172 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) |
|
Theorem | 3anbi2i 1173 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) ↔ (𝜒 ∧ 𝜓 ∧ 𝜃)) |
|
Theorem | 3anbi3i 1174 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓)) |
|
Theorem | 3imp 1175 |
Importation inference. (Contributed by NM, 8-Apr-1994.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3impa 1176 |
Importation from double to triple conjunction. (Contributed by NM,
20-Aug-1995.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3impb 1177 |
Importation from double to triple conjunction. (Contributed by NM,
20-Aug-1995.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3impia 1178 |
Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3impib 1179 |
Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3exp 1180 |
Exportation inference. (Contributed by NM, 30-May-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
|
Theorem | 3expa 1181 |
Exportation from triple to double conjunction. (Contributed by NM,
20-Aug-1995.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
|
Theorem | 3expb 1182 |
Exportation from triple to double conjunction. (Contributed by NM,
20-Aug-1995.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3expia 1183 |
Exportation from triple conjunction. (Contributed by NM,
19-May-2007.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
|
Theorem | 3expib 1184 |
Exportation from triple conjunction. (Contributed by NM,
19-May-2007.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
|
Theorem | 3com12 1185 |
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
|
Theorem | 3com13 1186 |
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28-Jan-1996.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) |
|
Theorem | 3com23 1187 |
Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM,
28-Jan-1996.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
|
Theorem | 3coml 1188 |
Commutation in antecedent. Rotate left. (Contributed by NM,
28-Jan-1996.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
|
Theorem | 3comr 1189 |
Commutation in antecedent. Rotate right. (Contributed by NM,
28-Jan-1996.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
|
Theorem | 3adant3r1 1190 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3adant3r2 1191 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
17-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3adant3r3 1192 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
18-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) |
|
Theorem | ad4ant123 1193 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜃) |
|
Theorem | ad4ant124 1194 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃) |
|
Theorem | ad4ant134 1195 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃) |
|
Theorem | ad4ant234 1196 |
Deduction adding conjuncts to antecedent. (Contributed by Alan Sare,
17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃) |
|
Theorem | 3an1rs 1197 |
Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒) → 𝜏) |
|
Theorem | 3imp1 1198 |
Importation to left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
|
Theorem | 3impd 1199 |
Importation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
|
Theorem | 3imp2 1200 |
Importation to right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) |