![]() |
Metamath
Proof Explorer Theorem List (p. 12 of 437) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28364) |
![]() (28365-29889) |
![]() (29890-43671) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3imp231 1101 | Importation inference. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) | ||
Theorem | 3imp21 1102 | The importation inference 3imp 1098 with commutation of the first and second conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.) (Revised to shorten 3com12 1114 by Wolf Lammen, 23-Jun-2022.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | 3impaOLD 1103 | Obsolete version of 3impa 1097 as of 20-Jun-2022. (Contributed by NM, 20-Aug-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3impb 1104 | Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3impib 1105 | Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3impia 1106 | Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3impiaOLD 1107 | Obsolete version of 3impia 1106 as of 21-Jun-2022. (Contributed by NM, 13-Jun-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3expa 1108 | Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3exp 1109 and pm3.2an3 1396 by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3exp 1109 | Exportation inference. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | ||
Theorem | 3expb 1110 | Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3expia 1111 | Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) | ||
Theorem | 3expiaOLD 1112 | Obsolete version of 3expia 1111 as of 22-Jun-2022. (Contributed by NM, 19-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) | ||
Theorem | 3expib 1113 | Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | ||
Theorem | 3com12 1114 | Commutation in antecedent. Swap 1st and 2nd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | 3com13 1115 | Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) | ||
Theorem | 3comr 1116 | Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.) (Revised by Wolf Lammen, 9-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) | ||
Theorem | 3com23 1117 | Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 9-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) | ||
Theorem | 3coml 1118 | Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) | ||
Theorem | 3jca 1119 | Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | 3jcad 1120 | Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏))) | ||
Theorem | 3adant1 1121 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) (Proof shortened by Wolf Lammen, 21-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | 3adant2 1122 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒) | ||
Theorem | 3adant3 1123 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) (Proof shortened by Wolf Lammen, 21-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | ||
Theorem | 3ad2ant1 1124 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | ||
Theorem | 3ad2ant2 1125 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒) | ||
Theorem | 3ad2ant3 1126 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒) | ||
Theorem | simp1 1127 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | ||
Theorem | simp2 1128 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | ||
Theorem | simp3 1129 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | ||
Theorem | simp1i 1130 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜑 | ||
Theorem | simp2i 1131 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜓 | ||
Theorem | simp3i 1132 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | simp1d 1133 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | simp2d 1134 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | simp3d 1135 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | simp1bi 1136 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | simp2bi 1137 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | simp3bi 1138 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | 3simpa 1139 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓)) | ||
Theorem | 3simpaOLD 1140 | Obsolete version of 3simpa 1139 as of 21-Jun-2022. (Contributed by NM, 21-Apr-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓)) | ||
Theorem | 3simpb 1141 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒)) | ||
Theorem | 3simpbOLD 1142 | Obsolete version of 3simpb 1141 as of 21-Jun-2022. (Contributed by NM, 21-Apr-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒)) | ||
Theorem | 3simpc 1143 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 21-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | ||
Theorem | 3simpcOLD 1144 | Obsolete version of 3simpc 1143 as of 21-Jun-2022. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | ||
Theorem | simp1OLD 1145 | Obsolete version of simp1 1127 as of 22-Jun-2022. (Contributed by NM, 21-Apr-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | ||
Theorem | simp2OLD 1146 | Obsolete version of simp2 1128 as of 22-Jun-2022. (Contributed by NM, 21-Apr-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | ||
Theorem | simp3OLD 1147 | Obsolete version of simp3 1129 as of 22-Jun-2022. (Contributed by NM, 21-Apr-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | ||
Theorem | 3adant1OLD 1148 | Obsolete version of 3adant1 1121 as of 21-Jun-2022. (Contributed by NM, 16-Jul-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | 3adant2OLD 1149 | Obsolete version of 3adant1 1121 as of 21-Jun-2022. (Contributed by NM, 16-Jul-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒) | ||
Theorem | 3adant3OLD 1150 | Obsolete version of 3adant3 1123 as of 21-Jun-2022. (Contributed by NM, 16-Jul-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | ||
Theorem | 3anim123i 1151 | Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜏 → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂)) | ||
Theorem | 3anim1i 1152 | Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | 3anim2i 1153 | Add two conjuncts to antecedent and consequent. (Contributed by AV, 21-Nov-2019.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
Theorem | 3anim3i 1154 | Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓)) | ||
Theorem | 3anbi123i 1155 | Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜏 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) | ||
Theorem | 3orbi123i 1156 | Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜏 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)) | ||
Theorem | 3anbi1i 1157 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | 3anbi2i 1158 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) ↔ (𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
Theorem | 3anbi3i 1159 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓)) | ||
Theorem | syl3an 1160 | A triple syllogism inference. (Contributed by NM, 13-May-2004.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜏 → 𝜂) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | syl3anb 1161 | A triple syllogism inference. (Contributed by NM, 15-Oct-2005.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜏 ↔ 𝜂) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | syl3anbr 1162 | A triple syllogism inference. (Contributed by NM, 29-Dec-2011.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜒) & ⊢ (𝜂 ↔ 𝜏) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | syl3an1 1163 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an2 1164 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.) |
⊢ (𝜑 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an2OLD 1165 | Obsolete version of syl3an2 1164 as of 26-Jun-2022. (Contributed by NM, 22-Aug-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an3 1166 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.) |
⊢ (𝜑 → 𝜃) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) | ||
Theorem | syl3an3OLD 1167 | Obsolete version of syl3an3 1166 as of 26-Jun-2022. (Contributed by NM, 22-Aug-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜃) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) | ||
Theorem | 3adantl1 1168 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adantl2 1169 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adantl3 1170 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adantr1 1171 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adantr2 1172 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adantr3 1173 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) | ||
Theorem | ad4ant123 1174 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜃) | ||
Theorem | ad4ant124 1175 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | ad4ant134 1176 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | ad4ant234 1177 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant1l 1178 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant1lOLD 1179 | Obsolete version of 3adant1l 1178 as of 23-Jun-2022. (Contributed by NM, 8-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant1r 1180 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant1rOLD 1181 | Obsolete version of 3adant1r 1180 as of 23-Jun-2022. (Contributed by NM, 8-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant2l 1182 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant2lOLD 1183 | Obsolete version of 3adant2l 1182 as of 25-Jun-2022. (Contributed by NM, 8-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant2r 1184 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant2rOLD 1185 | Obsolete version of 3adant2r 1184 as of 25-Jun-2022. (Contributed by NM, 8-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant3l 1186 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adant3lOLD 1187 | Obsolete version of 3adant3l 1186 as of 25-Jun-2022. (Contributed by NM, 8-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adant3r 1188 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) | ||
Theorem | 3adant3rOLD 1189 | Obsolete version of 3adant3r 1188 as of 25-Jun-2022. (Contributed by NM, 8-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) | ||
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 | 3ad2antl1 1193 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3ad2antl2 1194 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3ad2antl3 1195 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃) | ||
Theorem | 3ad2antr1 1196 | Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) | ||
Theorem | 3ad2antr2 1197 | Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) | ||
Theorem | 3ad2antr3 1198 | Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | simpl1 1199 | Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) | ||
Theorem | simpl1OLD 1200 | Obsolete version of simpl1 1199 as of 23-Jun-2022. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |