HomeTheorem List (p. 12 of 169)
GIF version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Intuitionistic Logic Explorer Theorem List (p. 12 of 169) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | simpl13 1101 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
| Theorem | simpl21 1102 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜑) | ||
| Theorem | simpl22 1103 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜓) | ||
| Theorem | simpl23 1104 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂) → 𝜒) | ||
| Theorem | simpl31 1105 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) | ||
| Theorem | simpl32 1106 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) | ||
| Theorem | simpl33 1107 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) | ||
| Theorem | simpr11 1108 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜑) | ||
| Theorem | simpr12 1109 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜓) | ||
| Theorem | simpr13 1110 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜒) | ||
| Theorem | simpr21 1111 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜑) | ||
| Theorem | simpr22 1112 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜓) | ||
| Theorem | simpr23 1113 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜒) | ||
| Theorem | simpr31 1114 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
| Theorem | simpr32 1115 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
| Theorem | simpr33 1116 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
| Theorem | simp1l1 1117 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
| Theorem | simp1l2 1118 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
| Theorem | simp1l3 1119 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜒) | ||
| Theorem | simp1r1 1120 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
| Theorem | simp1r2 1121 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
| Theorem | simp1r3 1122 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜏 ∧ 𝜂) → 𝜒) | ||
| Theorem | simp2l1 1123 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜑) | ||
| Theorem | simp2l2 1124 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜓) | ||
| Theorem | simp2l3 1125 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜂) → 𝜒) | ||
| Theorem | simp2r1 1126 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑) | ||
| Theorem | simp2r2 1127 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓) | ||
| Theorem | simp2r3 1128 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒) | ||
| Theorem | simp3l1 1129 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑) | ||
| Theorem | simp3l2 1130 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜓) | ||
| Theorem | simp3l3 1131 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒) | ||
| Theorem | simp3r1 1132 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
| Theorem | simp3r2 1133 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
| Theorem | simp3r3 1134 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
| Theorem | simp11l 1135 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
| Theorem | simp11r 1136 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
| Theorem | simp12l 1137 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
| Theorem | simp12r 1138 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
| Theorem | simp13l 1139 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜑) | ||
| Theorem | simp13r 1140 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜏 ∧ 𝜂) → 𝜓) | ||
| Theorem | simp21l 1141 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜑) | ||
| Theorem | simp21r 1142 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜂) → 𝜓) | ||
| Theorem | simp22l 1143 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜑) | ||
| Theorem | simp22r 1144 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜂) → 𝜓) | ||
| Theorem | simp23l 1145 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜑) | ||
| Theorem | simp23r 1146 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓)) ∧ 𝜂) → 𝜓) | ||
| Theorem | simp31l 1147 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑) | ||
| Theorem | simp31r 1148 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓) | ||
| Theorem | simp32l 1149 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑) | ||
| Theorem | simp32r 1150 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜓) | ||
| Theorem | simp33l 1151 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜑) | ||
| Theorem | simp33r 1152 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜏 ∧ 𝜂 ∧ (𝜒 ∧ 𝜃 ∧ (𝜑 ∧ 𝜓))) → 𝜓) | ||
| Theorem | simp111 1153 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑) | ||
| Theorem | simp112 1154 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓) | ||
| Theorem | simp113 1155 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒) | ||
| Theorem | simp121 1156 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜑) | ||
| Theorem | simp122 1157 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜓) | ||
| Theorem | simp123 1158 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜂 ∧ 𝜁) → 𝜒) | ||
| Theorem | simp131 1159 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜑) | ||
| Theorem | simp132 1160 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜓) | ||
| Theorem | simp133 1161 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂 ∧ 𝜁) → 𝜒) | ||
| Theorem | simp211 1162 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜑) | ||
| Theorem | simp212 1163 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜓) | ||
| Theorem | simp213 1164 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜁) → 𝜒) | ||
| Theorem | simp221 1165 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜑) | ||
| Theorem | simp222 1166 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜓) | ||
| Theorem | simp223 1167 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏) ∧ 𝜁) → 𝜒) | ||
| Theorem | simp231 1168 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜑) | ||
| Theorem | simp232 1169 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜓) | ||
| Theorem | simp233 1170 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜁) → 𝜒) | ||
| Theorem | simp311 1171 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜑) | ||
| Theorem | simp312 1172 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜓) | ||
| Theorem | simp313 1173 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏)) → 𝜒) | ||
| Theorem | simp321 1174 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜑) | ||
| Theorem | simp322 1175 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜓) | ||
| Theorem | simp323 1176 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜏)) → 𝜒) | ||
| Theorem | simp331 1177 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) | ||
| Theorem | simp332 1178 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) | ||
| Theorem | simp333 1179 | Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) |
| ⊢ ((𝜂 ∧ 𝜁 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) | ||
| Theorem | 3adantl1 1180 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
| Theorem | 3adantl2 1181 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
| Theorem | 3adantl3 1182 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
| ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
| Theorem | 3adantr1 1183 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) | ||
| Theorem | 3adantr2 1184 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) | ||
| Theorem | 3adantr3 1185 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
| ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) | ||
| Theorem | 3ad2antl1 1186 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
| ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
| Theorem | 3ad2antl2 1187 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
| ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
| Theorem | 3ad2antl3 1188 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
| ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃) | ||
| Theorem | 3ad2antr1 1189 | Deduction adding a conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.) |
| ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) | ||
| Theorem | 3ad2antr2 1190 | Deduction adding a conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.) |
| ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) | ||
| Theorem | 3ad2antr3 1191 | Deduction adding a conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.) |
| ⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) | ||
| Theorem | 3anibar 1192 | Remove a hypothesis from the second member of a biconditional. (Contributed by FL, 22-Jul-2008.) |
| ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ (𝜒 ∧ 𝜏))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) | ||
| Theorem | 3mix1 1193 | Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
| ⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) | ||
| Theorem | 3mix2 1194 | Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
| ⊢ (𝜑 → (𝜓 ∨ 𝜑 ∨ 𝜒)) | ||
| Theorem | 3mix3 1195 | Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.) |
| ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑)) | ||
| Theorem | 3mix1i 1196 | Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.) |
| ⊢ 𝜑 ⇒ ⊢ (𝜑 ∨ 𝜓 ∨ 𝜒) | ||
| Theorem | 3mix2i 1197 | Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.) |
| ⊢ 𝜑 ⇒ ⊢ (𝜓 ∨ 𝜑 ∨ 𝜒) | ||
| Theorem | 3mix3i 1198 | Introduction in triple disjunction. (Contributed by Mario Carneiro, 6-Oct-2014.) |
| ⊢ 𝜑 ⇒ ⊢ (𝜓 ∨ 𝜒 ∨ 𝜑) | ||
| Theorem | 3mix1d 1199 | Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃)) | ||
| Theorem | 3mix2d 1200 | Deduction introducing triple disjunction. (Contributed by Scott Fenton, 8-Jun-2011.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |