 Home Metamath Proof ExplorerTheorem 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: Metamath Proof Explorer (1-28364) Hilbert Space Explorer (28365-29889) Users' Mathboxes (29890-43671)

Theorem List for Metamath Proof Explorer - 1101-1200   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theorem3imp231 1101 Importation inference. (Contributed by Alan Sare, 17-Oct-2017.)
(𝜑 → (𝜓 → (𝜒𝜃)))       ((𝜓𝜒𝜑) → 𝜃)

Theorem3imp21 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.)
(𝜑 → (𝜓 → (𝜒𝜃)))       ((𝜓𝜑𝜒) → 𝜃)

Theorem3impaOLD 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.)
(((𝜑𝜓) ∧ 𝜒) → 𝜃)       ((𝜑𝜓𝜒) → 𝜃)

Theorem3impb 1104 Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
((𝜑 ∧ (𝜓𝜒)) → 𝜃)       ((𝜑𝜓𝜒) → 𝜃)

Theorem3impib 1105 Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
(𝜑 → ((𝜓𝜒) → 𝜃))       ((𝜑𝜓𝜒) → 𝜃)

Theorem3impia 1106 Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
((𝜑𝜓) → (𝜒𝜃))       ((𝜑𝜓𝜒) → 𝜃)

Theorem3impiaOLD 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.)
((𝜑𝜓) → (𝜒𝜃))       ((𝜑𝜓𝜒) → 𝜃)

Theorem3expa 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.)
((𝜑𝜓𝜒) → 𝜃)       (((𝜑𝜓) ∧ 𝜒) → 𝜃)

Theorem3exp 1109 Exportation inference. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
((𝜑𝜓𝜒) → 𝜃)       (𝜑 → (𝜓 → (𝜒𝜃)))

Theorem3expb 1110 Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑 ∧ (𝜓𝜒)) → 𝜃)

Theorem3expia 1111 Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑𝜓) → (𝜒𝜃))

Theorem3expiaOLD 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.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑𝜓) → (𝜒𝜃))

Theorem3expib 1113 Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)
((𝜑𝜓𝜒) → 𝜃)       (𝜑 → ((𝜓𝜒) → 𝜃))

Theorem3com12 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.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜓𝜑𝜒) → 𝜃)

Theorem3com13 1115 Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜒𝜓𝜑) → 𝜃)

Theorem3comr 1116 Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.) (Revised by Wolf Lammen, 9-Apr-2022.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜒𝜑𝜓) → 𝜃)

Theorem3com23 1117 Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM, 28-Jan-1996.) (Proof shortened by Wolf Lammen, 9-Apr-2022.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑𝜒𝜓) → 𝜃)

Theorem3coml 1118 Commutation in antecedent. Rotate left. (Contributed by NM, 28-Jan-1996.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜓𝜒𝜑) → 𝜃)

Theorem3jca 1119 Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
(𝜑𝜓)    &   (𝜑𝜒)    &   (𝜑𝜃)       (𝜑 → (𝜓𝜒𝜃))

Theorem3jcad 1120 Deduction conjoining the consequents of three implications. (Contributed by NM, 25-Sep-2005.)
(𝜑 → (𝜓𝜒))    &   (𝜑 → (𝜓𝜃))    &   (𝜑 → (𝜓𝜏))       (𝜑 → (𝜓 → (𝜒𝜃𝜏)))

Theorem3adant1 1121 Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
((𝜑𝜓) → 𝜒)       ((𝜃𝜑𝜓) → 𝜒)

Theorem3adant2 1122 Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
((𝜑𝜓) → 𝜒)       ((𝜑𝜃𝜓) → 𝜒)

Theorem3adant3 1123 Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
((𝜑𝜓) → 𝜒)       ((𝜑𝜓𝜃) → 𝜒)

Theorem3ad2ant1 1124 Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
(𝜑𝜒)       ((𝜑𝜓𝜃) → 𝜒)

Theorem3ad2ant2 1125 Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
(𝜑𝜒)       ((𝜓𝜑𝜃) → 𝜒)

Theorem3ad2ant3 1126 Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)
(𝜑𝜒)       ((𝜓𝜃𝜑) → 𝜒)

Theoremsimp1 1127 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
((𝜑𝜓𝜒) → 𝜑)

Theoremsimp2 1128 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
((𝜑𝜓𝜒) → 𝜓)

Theoremsimp3 1129 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)
((𝜑𝜓𝜒) → 𝜒)

Theoremsimp1i 1130 Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
(𝜑𝜓𝜒)       𝜑

Theoremsimp2i 1131 Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
(𝜑𝜓𝜒)       𝜓

Theoremsimp3i 1132 Infer a conjunct from a triple conjunction. (Contributed by NM, 19-Apr-2005.)
(𝜑𝜓𝜒)       𝜒

Theoremsimp1d 1133 Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
(𝜑 → (𝜓𝜒𝜃))       (𝜑𝜓)

Theoremsimp2d 1134 Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
(𝜑 → (𝜓𝜒𝜃))       (𝜑𝜒)

Theoremsimp3d 1135 Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
(𝜑 → (𝜓𝜒𝜃))       (𝜑𝜃)

Theoremsimp1bi 1136 Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(𝜑 ↔ (𝜓𝜒𝜃))       (𝜑𝜓)

Theoremsimp2bi 1137 Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(𝜑 ↔ (𝜓𝜒𝜃))       (𝜑𝜒)

Theoremsimp3bi 1138 Deduce a conjunct from a triple conjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
(𝜑 ↔ (𝜓𝜒𝜃))       (𝜑𝜃)

Theorem3simpa 1139 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
((𝜑𝜓𝜒) → (𝜑𝜓))

Theorem3simpaOLD 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.)
((𝜑𝜓𝜒) → (𝜑𝜓))

Theorem3simpb 1141 Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)
((𝜑𝜓𝜒) → (𝜑𝜒))

Theorem3simpbOLD 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.)
((𝜑𝜓𝜒) → (𝜑𝜒))

Theorem3simpc 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.)
((𝜑𝜓𝜒) → (𝜓𝜒))

Theorem3simpcOLD 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.)
((𝜑𝜓𝜒) → (𝜓𝜒))

Theoremsimp1OLD 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.)
((𝜑𝜓𝜒) → 𝜑)

Theoremsimp2OLD 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.)
((𝜑𝜓𝜒) → 𝜓)

Theoremsimp3OLD 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.)
((𝜑𝜓𝜒) → 𝜒)

Theorem3adant1OLD 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.)
((𝜑𝜓) → 𝜒)       ((𝜃𝜑𝜓) → 𝜒)

Theorem3adant2OLD 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.)
((𝜑𝜓) → 𝜒)       ((𝜑𝜃𝜓) → 𝜒)

Theorem3adant3OLD 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.)
((𝜑𝜓) → 𝜒)       ((𝜑𝜓𝜃) → 𝜒)

Theorem3anim123i 1151 Join antecedents and consequents with conjunction. (Contributed by NM, 8-Apr-1994.)
(𝜑𝜓)    &   (𝜒𝜃)    &   (𝜏𝜂)       ((𝜑𝜒𝜏) → (𝜓𝜃𝜂))

Theorem3anim1i 1152 Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 16-Aug-2009.)
(𝜑𝜓)       ((𝜑𝜒𝜃) → (𝜓𝜒𝜃))

Theorem3anim2i 1153 Add two conjuncts to antecedent and consequent. (Contributed by AV, 21-Nov-2019.)
(𝜑𝜓)       ((𝜒𝜑𝜃) → (𝜒𝜓𝜃))

Theorem3anim3i 1154 Add two conjuncts to antecedent and consequent. (Contributed by Jeff Hankins, 19-Aug-2009.)
(𝜑𝜓)       ((𝜒𝜃𝜑) → (𝜒𝜃𝜓))

Theorem3anbi123i 1155 Join 3 biconditionals with conjunction. (Contributed by NM, 21-Apr-1994.)
(𝜑𝜓)    &   (𝜒𝜃)    &   (𝜏𝜂)       ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))

Theorem3orbi123i 1156 Join 3 biconditionals with disjunction. (Contributed by NM, 17-May-1994.)
(𝜑𝜓)    &   (𝜒𝜃)    &   (𝜏𝜂)       ((𝜑𝜒𝜏) ↔ (𝜓𝜃𝜂))

Theorem3anbi1i 1157 Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
(𝜑𝜓)       ((𝜑𝜒𝜃) ↔ (𝜓𝜒𝜃))

Theorem3anbi2i 1158 Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
(𝜑𝜓)       ((𝜒𝜑𝜃) ↔ (𝜒𝜓𝜃))

Theorem3anbi3i 1159 Inference adding two conjuncts to each side of a biconditional. (Contributed by NM, 8-Sep-2006.)
(𝜑𝜓)       ((𝜒𝜃𝜑) ↔ (𝜒𝜃𝜓))

Theoremsyl3an 1160 A triple syllogism inference. (Contributed by NM, 13-May-2004.)
(𝜑𝜓)    &   (𝜒𝜃)    &   (𝜏𝜂)    &   ((𝜓𝜃𝜂) → 𝜁)       ((𝜑𝜒𝜏) → 𝜁)

Theoremsyl3anb 1161 A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
(𝜑𝜓)    &   (𝜒𝜃)    &   (𝜏𝜂)    &   ((𝜓𝜃𝜂) → 𝜁)       ((𝜑𝜒𝜏) → 𝜁)

Theoremsyl3anbr 1162 A triple syllogism inference. (Contributed by NM, 29-Dec-2011.)
(𝜓𝜑)    &   (𝜃𝜒)    &   (𝜂𝜏)    &   ((𝜓𝜃𝜂) → 𝜁)       ((𝜑𝜒𝜏) → 𝜁)

Theoremsyl3an1 1163 A syllogism inference. (Contributed by NM, 22-Aug-1995.)
(𝜑𝜓)    &   ((𝜓𝜒𝜃) → 𝜏)       ((𝜑𝜒𝜃) → 𝜏)

Theoremsyl3an2 1164 A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)
(𝜑𝜒)    &   ((𝜓𝜒𝜃) → 𝜏)       ((𝜓𝜑𝜃) → 𝜏)

Theoremsyl3an2OLD 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.)
(𝜑𝜒)    &   ((𝜓𝜒𝜃) → 𝜏)       ((𝜓𝜑𝜃) → 𝜏)

Theoremsyl3an3 1166 A syllogism inference. (Contributed by NM, 22-Aug-1995.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)
(𝜑𝜃)    &   ((𝜓𝜒𝜃) → 𝜏)       ((𝜓𝜒𝜑) → 𝜏)

Theoremsyl3an3OLD 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.)
(𝜑𝜃)    &   ((𝜓𝜒𝜃) → 𝜏)       ((𝜓𝜒𝜑) → 𝜏)

Theorem3adantl1 1168 Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
(((𝜑𝜓) ∧ 𝜒) → 𝜃)       (((𝜏𝜑𝜓) ∧ 𝜒) → 𝜃)

Theorem3adantl2 1169 Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
(((𝜑𝜓) ∧ 𝜒) → 𝜃)       (((𝜑𝜏𝜓) ∧ 𝜒) → 𝜃)

Theorem3adantl3 1170 Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.)
(((𝜑𝜓) ∧ 𝜒) → 𝜃)       (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)

Theorem3adantr1 1171 Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
((𝜑 ∧ (𝜓𝜒)) → 𝜃)       ((𝜑 ∧ (𝜏𝜓𝜒)) → 𝜃)

Theorem3adantr2 1172 Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
((𝜑 ∧ (𝜓𝜒)) → 𝜃)       ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)

Theorem3adantr3 1173 Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.)
((𝜑 ∧ (𝜓𝜒)) → 𝜃)       ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)

Theoremad4ant123 1174 Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
((𝜑𝜓𝜒) → 𝜃)       ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜏) → 𝜃)

Theoremad4ant124 1175 Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
((𝜑𝜓𝜒) → 𝜃)       ((((𝜑𝜓) ∧ 𝜏) ∧ 𝜒) → 𝜃)

Theoremad4ant134 1176 Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
((𝜑𝜓𝜒) → 𝜃)       ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Theoremad4ant234 1177 Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)
((𝜑𝜓𝜒) → 𝜃)       ((((𝜏𝜑) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Theorem3adant1l 1178 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
((𝜑𝜓𝜒) → 𝜃)       (((𝜏𝜑) ∧ 𝜓𝜒) → 𝜃)

Theorem3adant1lOLD 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.)
((𝜑𝜓𝜒) → 𝜃)       (((𝜏𝜑) ∧ 𝜓𝜒) → 𝜃)

Theorem3adant1r 1180 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
((𝜑𝜓𝜒) → 𝜃)       (((𝜑𝜏) ∧ 𝜓𝜒) → 𝜃)

Theorem3adant1rOLD 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.)
((𝜑𝜓𝜒) → 𝜃)       (((𝜑𝜏) ∧ 𝜓𝜒) → 𝜃)

Theorem3adant2l 1182 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑 ∧ (𝜏𝜓) ∧ 𝜒) → 𝜃)

Theorem3adant2lOLD 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.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑 ∧ (𝜏𝜓) ∧ 𝜒) → 𝜃)

Theorem3adant2r 1184 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑 ∧ (𝜓𝜏) ∧ 𝜒) → 𝜃)

Theorem3adant2rOLD 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.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑 ∧ (𝜓𝜏) ∧ 𝜒) → 𝜃)

Theorem3adant3l 1186 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑𝜓 ∧ (𝜏𝜒)) → 𝜃)

Theorem3adant3lOLD 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.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑𝜓 ∧ (𝜏𝜒)) → 𝜃)

Theorem3adant3r 1188 Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)

Theorem3adant3rOLD 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.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑𝜓 ∧ (𝜒𝜏)) → 𝜃)

Theorem3adant3r1 1190 Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑 ∧ (𝜏𝜓𝜒)) → 𝜃)

Theorem3adant3r2 1191 Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑 ∧ (𝜓𝜏𝜒)) → 𝜃)

Theorem3adant3r3 1192 Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.)
((𝜑𝜓𝜒) → 𝜃)       ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)

((𝜑𝜒) → 𝜃)       (((𝜑𝜓𝜏) ∧ 𝜒) → 𝜃)

((𝜑𝜒) → 𝜃)       (((𝜓𝜑𝜏) ∧ 𝜒) → 𝜃)

((𝜑𝜒) → 𝜃)       (((𝜓𝜏𝜑) ∧ 𝜒) → 𝜃)

((𝜑𝜒) → 𝜃)       ((𝜑 ∧ (𝜒𝜓𝜏)) → 𝜃)

((𝜑𝜒) → 𝜃)       ((𝜑 ∧ (𝜓𝜒𝜏)) → 𝜃)