Home | Metamath
Proof Explorer Theorem List (p. 12 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3oran 1101 | Triple disjunction in terms of triple conjunction. (Contributed by NM, 8-Oct-2012.) |
⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ¬ (¬ 𝜑 ∧ ¬ 𝜓 ∧ ¬ 𝜒)) | ||
Theorem | 3impa 1102 | Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3imp 1103 by Wolf Lammen, 20-Jun-2022.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3imp 1103 | Importation inference. (Contributed by NM, 8-Apr-1994.) (Proof shortened by Wolf Lammen, 20-Jun-2022.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3imp31 1104 | The importation inference 3imp 1103 with commutation of the first and third conjuncts of the assertion relative to the hypothesis. (Contributed by Alan Sare, 11-Sep-2016.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) | ||
Theorem | 3imp231 1105 | Importation inference. (Contributed by Alan Sare, 17-Oct-2017.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) | ||
Theorem | 3imp21 1106 | The importation inference 3imp 1103 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 1115 by Wolf Lammen, 23-Jun-2022.) |
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) | ||
Theorem | 3impb 1107 | Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3impib 1108 | Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) |
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3impia 1109 | Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3expa 1110 | Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3exp 1111 and pm3.2an3 1332 by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3exp 1111 | Exportation inference. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | ||
Theorem | 3expb 1112 | Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3expia 1113 | Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) | ||
Theorem | 3expib 1114 | Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | ||
Theorem | 3com12 1115 | 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 1116 | Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) | ||
Theorem | 3comr 1117 | Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.) (Revised by Wolf Lammen, 9-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) | ||
Theorem | 3com23 1118 | Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 9-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) | ||
Theorem | 3coml 1119 | Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) | ||
Theorem | 3jca 1120 | Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜑 → 𝜒) & ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | 3jcad 1121 | Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏))) | ||
Theorem | 3adant1 1122 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) (Proof shortened by Wolf Lammen, 21-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜃 ∧ 𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | 3adant2 1123 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜃 ∧ 𝜓) → 𝜒) | ||
Theorem | 3adant3 1124 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) (Proof shortened by Wolf Lammen, 21-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | ||
Theorem | 3ad2ant1 1125 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜒) | ||
Theorem | 3ad2ant2 1126 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒) | ||
Theorem | 3ad2ant3 1127 | Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.) |
⊢ (𝜑 → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜑) → 𝜒) | ||
Theorem | simp1 1128 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑) | ||
Theorem | simp2 1129 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓) | ||
Theorem | simp3 1130 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒) | ||
Theorem | simp1i 1131 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜑 | ||
Theorem | simp2i 1132 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜓 | ||
Theorem | simp3i 1133 | Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.) |
⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) ⇒ ⊢ 𝜒 | ||
Theorem | simp1d 1134 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | simp2d 1135 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | simp3d 1136 | Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | simp1bi 1137 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | simp2bi 1138 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | simp3bi 1139 | Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | 3simpa 1140 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓)) | ||
Theorem | 3simpb 1141 | Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜒)) | ||
Theorem | 3simpc 1142 | 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 | 3anim123i 1143 | Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜏 → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂)) | ||
Theorem | 3anim1i 1144 | Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | 3anim2i 1145 | Add two conjuncts to antecedent and consequent. (Contributed by AV, 21-Nov-2019.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
Theorem | 3anim3i 1146 | Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓)) | ||
Theorem | 3anbi123i 1147 | Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜏 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) | ||
Theorem | 3orbi123i 1148 | Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜏 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)) | ||
Theorem | 3anbi1i 1149 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | 3anbi2i 1150 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) ↔ (𝜒 ∧ 𝜓 ∧ 𝜃)) | ||
Theorem | 3anbi3i 1151 | Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓)) | ||
Theorem | syl3an 1152 | A triple syllogism inference. (Contributed by NM, 13-May-2004.) |
⊢ (𝜑 → 𝜓) & ⊢ (𝜒 → 𝜃) & ⊢ (𝜏 → 𝜂) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | syl3anb 1153 | A triple syllogism inference. (Contributed by NM, 15-Oct-2005.) |
⊢ (𝜑 ↔ 𝜓) & ⊢ (𝜒 ↔ 𝜃) & ⊢ (𝜏 ↔ 𝜂) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | syl3anbr 1154 | A triple syllogism inference. (Contributed by NM, 29-Dec-2011.) |
⊢ (𝜓 ↔ 𝜑) & ⊢ (𝜃 ↔ 𝜒) & ⊢ (𝜂 ↔ 𝜏) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁) | ||
Theorem | syl3an1 1155 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) |
⊢ (𝜑 → 𝜓) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an2 1156 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.) |
⊢ (𝜑 → 𝜒) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜏) | ||
Theorem | syl3an3 1157 | A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.) |
⊢ (𝜑 → 𝜃) & ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜏) | ||
Theorem | 3adantl1 1158 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adantl2 1159 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adantl3 1160 | Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adantr1 1161 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adantr2 1162 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adantr3 1163 | Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) | ||
Theorem | ad4ant123 1164 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜃) | ||
Theorem | ad4ant124 1165 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | ad4ant134 1166 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | ad4ant234 1167 | Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((((𝜏 ∧ 𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant1l 1168 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant1r 1169 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant2l 1170 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant2r 1171 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3adant3l 1172 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adant3r 1173 | Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) | ||
Theorem | 3adant3r1 1174 | Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adant3r2 1175 | Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | 3adant3r3 1176 | Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.) |
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) | ||
Theorem | 3ad2antl1 1177 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3ad2antl2 1178 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) | ||
Theorem | 3ad2antl3 1179 | Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃) | ||
Theorem | 3ad2antr1 1180 | Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) | ||
Theorem | 3ad2antr2 1181 | Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) | ||
Theorem | 3ad2antr3 1182 | Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.) |
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) | ||
Theorem | simpl1 1183 | Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑) | ||
Theorem | simpl2 1184 | Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | ||
Theorem | simpl3 1185 | Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) | ||
Theorem | simpr1 1186 | Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜓) | ||
Theorem | simpr2 1187 | Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜒) | ||
Theorem | simpr3 1188 | Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜃) | ||
Theorem | simp1l 1189 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑) | ||
Theorem | simp1r 1190 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜓) | ||
Theorem | simp2l 1191 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓) | ||
Theorem | simp2r 1192 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒) | ||
Theorem | simp3l 1193 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜒) | ||
Theorem | simp3r 1194 | Simplification of triple conjunction. (Contributed by NM, 9-Nov-2011.) |
⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜃) | ||
Theorem | simp11 1195 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜑) | ||
Theorem | simp12 1196 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜓) | ||
Theorem | simp13 1197 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒) | ||
Theorem | simp21 1198 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓) | ||
Theorem | simp22 1199 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜒) | ||
Theorem | simp23 1200 | Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.) |
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜃) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |