Theorem List for Intuitionistic Logic Explorer - 1101-1200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 3ad2antl2 1101 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
|
Theorem | 3ad2antl3 1102 |
Deduction adding conjuncts to antecedent. (Contributed by NM,
4-Aug-2007.)
|
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃) |
|
Theorem | 3ad2antr1 1103 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
25-Dec-2007.)
|
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃) |
|
Theorem | 3ad2antr2 1104 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
27-Dec-2007.)
|
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) |
|
Theorem | 3ad2antr3 1105 |
Deduction adding a conjuncts to antecedent. (Contributed by NM,
30-Dec-2007.)
|
⊢ ((𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3anibar 1106 |
Remove a hypothesis from the second member of a biimplication.
(Contributed by FL, 22-Jul-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ (𝜒 ∧ 𝜏))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) |
|
Theorem | 3mix1 1107 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
⊢ (𝜑 → (𝜑 ∨ 𝜓 ∨ 𝜒)) |
|
Theorem | 3mix2 1108 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
⊢ (𝜑 → (𝜓 ∨ 𝜑 ∨ 𝜒)) |
|
Theorem | 3mix3 1109 |
Introduction in triple disjunction. (Contributed by NM, 4-Apr-1995.)
|
⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜑)) |
|
Theorem | 3mix1i 1110 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
⊢ 𝜑 ⇒ ⊢ (𝜑 ∨ 𝜓 ∨ 𝜒) |
|
Theorem | 3mix2i 1111 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
⊢ 𝜑 ⇒ ⊢ (𝜓 ∨ 𝜑 ∨ 𝜒) |
|
Theorem | 3mix3i 1112 |
Introduction in triple disjunction. (Contributed by Mario Carneiro,
6-Oct-2014.)
|
⊢ 𝜑 ⇒ ⊢ (𝜓 ∨ 𝜒 ∨ 𝜑) |
|
Theorem | 3mix1d 1113 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃)) |
|
Theorem | 3mix2d 1114 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃)) |
|
Theorem | 3mix3d 1115 |
Deduction introducing triple disjunction. (Contributed by Scott Fenton,
8-Jun-2011.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → (𝜒 ∨ 𝜃 ∨ 𝜓)) |
|
Theorem | 3pm3.2i 1116 |
Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)
|
⊢ 𝜑
& ⊢ 𝜓
& ⊢ 𝜒 ⇒ ⊢ (𝜑 ∧ 𝜓 ∧ 𝜒) |
|
Theorem | pm3.2an3 1117 |
pm3.2 137 for a triple conjunction. (Contributed by
Alan Sare,
24-Oct-2011.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 ∧ 𝜓 ∧ 𝜒)))) |
|
Theorem | 3jca 1118 |
Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
|
Theorem | 3jcad 1119 |
Deduction conjoining the consequents of three implications.
(Contributed by NM, 25-Sep-2005.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃 ∧ 𝜏))) |
|
Theorem | mpbir3an 1120 |
Detach a conjunction of truths in a biconditional. (Contributed by NM,
16-Sep-2011.) (Revised by NM, 9-Jan-2015.)
|
⊢ 𝜓
& ⊢ 𝜒
& ⊢ 𝜃
& ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ 𝜑 |
|
Theorem | mpbir3and 1121 |
Detach a conjunction of truths in a biconditional. (Contributed by
Mario Carneiro, 11-May-2014.)
|
⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | syl3anbrc 1122 |
Syllogism inference. (Contributed by Mario Carneiro, 11-May-2014.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜏 ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) ⇒ ⊢ (𝜑 → 𝜏) |
|
Theorem | 3anim123i 1123 |
Join antecedents and consequents with conjunction. (Contributed by NM,
8-Apr-1994.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜒 → 𝜃)
& ⊢ (𝜏 → 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂)) |
|
Theorem | 3anim1i 1124 |
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 16-Aug-2009.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
|
Theorem | 3anim2i 1125 |
Add two conjuncts to antecedent and consequent. (Contributed by AV,
21-Nov-2019.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) → (𝜒 ∧ 𝜓 ∧ 𝜃)) |
|
Theorem | 3anim3i 1126 |
Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 19-Aug-2009.)
|
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) → (𝜒 ∧ 𝜃 ∧ 𝜓)) |
|
Theorem | 3anbi123i 1127 |
Join 3 biconditionals with conjunction. (Contributed by NM,
21-Apr-1994.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ (𝜒 ↔ 𝜃)
& ⊢ (𝜏 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) ↔ (𝜓 ∧ 𝜃 ∧ 𝜂)) |
|
Theorem | 3orbi123i 1128 |
Join 3 biconditionals with disjunction. (Contributed by NM,
17-May-1994.)
|
⊢ (𝜑 ↔ 𝜓)
& ⊢ (𝜒 ↔ 𝜃)
& ⊢ (𝜏 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)) |
|
Theorem | 3anbi1i 1129 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜃) ↔ (𝜓 ∧ 𝜒 ∧ 𝜃)) |
|
Theorem | 3anbi2i 1130 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜃) ↔ (𝜒 ∧ 𝜓 ∧ 𝜃)) |
|
Theorem | 3anbi3i 1131 |
Inference adding two conjuncts to each side of a biconditional.
(Contributed by NM, 8-Sep-2006.)
|
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ((𝜒 ∧ 𝜃 ∧ 𝜑) ↔ (𝜒 ∧ 𝜃 ∧ 𝜓)) |
|
Theorem | 3imp 1132 |
Importation inference. (Contributed by NM, 8-Apr-1994.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3impa 1133 |
Importation from double to triple conjunction. (Contributed by NM,
20-Aug-1995.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3impb 1134 |
Importation from double to triple conjunction. (Contributed by NM,
20-Aug-1995.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3impia 1135 |
Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|
⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3impib 1136 |
Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3exp 1137 |
Exportation inference. (Contributed by NM, 30-May-1994.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
|
Theorem | 3expa 1138 |
Exportation from triple to double conjunction. (Contributed by NM,
20-Aug-1995.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
|
Theorem | 3expb 1139 |
Exportation from triple to double conjunction. (Contributed by NM,
20-Aug-1995.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3expia 1140 |
Exportation from triple conjunction. (Contributed by NM,
19-May-2007.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
|
Theorem | 3expib 1141 |
Exportation from triple conjunction. (Contributed by NM,
19-May-2007.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
|
Theorem | 3com12 1142 |
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28-Jan-1996.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
|
Theorem | 3com13 1143 |
Commutation in antecedent. Swap 1st and 3rd. (Contributed by NM,
28-Jan-1996.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) |
|
Theorem | 3com23 1144 |
Commutation in antecedent. Swap 2nd and 3rd. (Contributed by NM,
28-Jan-1996.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
|
Theorem | 3coml 1145 |
Commutation in antecedent. Rotate left. (Contributed by NM,
28-Jan-1996.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) |
|
Theorem | 3comr 1146 |
Commutation in antecedent. Rotate right. (Contributed by NM,
28-Jan-1996.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) |
|
Theorem | 3adant3r1 1147 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
16-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3adant3r2 1148 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
17-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3adant3r3 1149 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
18-Feb-2008.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) |
|
Theorem | 3an1rs 1150 |
Swap conjuncts. (Contributed by NM, 16-Dec-2007.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜃) ∧ 𝜒) → 𝜏) |
|
Theorem | 3imp1 1151 |
Importation to left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
|
Theorem | 3impd 1152 |
Importation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
|
Theorem | 3imp2 1153 |
Importation to right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) |
|
Theorem | 3exp1 1154 |
Exportation from left triple conjunction. (Contributed by NM,
24-Feb-2005.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
|
Theorem | 3expd 1155 |
Exportation deduction for triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
|
Theorem | 3exp2 1156 |
Exportation from right triple conjunction. (Contributed by NM,
26-Oct-2006.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
|
Theorem | exp5o 1157 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ((𝜃 ∧ 𝜏) → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) |
|
Theorem | exp516 1158 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) |
|
Theorem | exp520 1159 |
A triple exportation inference. (Contributed by Jeff Hankins,
8-Jul-2009.)
|
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))) |
|
Theorem | 3anassrs 1160 |
Associative law for conjunction applied to antecedent (eliminates
syllogism). (Contributed by Mario Carneiro, 4-Jan-2017.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏) |
|
Theorem | 3adant1l 1161 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3adant1r 1162 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | 3adant2l 1163 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
|
Theorem | 3adant2r 1164 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
|
Theorem | 3adant3l 1165 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃) |
|
Theorem | 3adant3r 1166 |
Deduction adding a conjunct to antecedent. (Contributed by NM,
8-Jan-2006.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃) |
|
Theorem | syl12anc 1167 |
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1-Aug-2009.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃)) → 𝜏) ⇒ ⊢ (𝜑 → 𝜏) |
|
Theorem | syl21anc 1168 |
Syllogism combined with contraction. (Contributed by Jeff Hankins,
1-Aug-2009.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → 𝜏) |
|
Theorem | syl3anc 1169 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → 𝜏) |
|
Theorem | syl22anc 1170 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl13anc 1171 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl31anc 1172 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl112anc 1173 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏)) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl121anc 1174 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl211anc 1175 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → 𝜂) |
|
Theorem | syl23anc 1176 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl32anc 1177 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl122anc 1178 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl212anc 1179 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl221anc 1180 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl113anc 1181 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ ((𝜓 ∧ 𝜒 ∧ (𝜃 ∧ 𝜏 ∧ 𝜂)) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl131anc 1182 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl311anc 1183 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁) ⇒ ⊢ (𝜑 → 𝜁) |
|
Theorem | syl33anc 1184 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl222anc 1185 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl123anc 1186 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl132anc 1187 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl213anc 1188 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl231anc 1189 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl312anc 1190 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁)) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl321anc 1191 |
Syllogism combined with contraction. (Contributed by NM,
11-Jul-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ 𝜁) → 𝜎) ⇒ ⊢ (𝜑 → 𝜎) |
|
Theorem | syl133anc 1192 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl313anc 1193 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl331anc 1194 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ 𝜎) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl223anc 1195 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl232anc 1196 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl322anc 1197 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎)) → 𝜌) ⇒ ⊢ (𝜑 → 𝜌) |
|
Theorem | syl233anc 1198 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (𝜑 → 𝜌)
& ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) |
|
Theorem | syl323anc 1199 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (𝜑 → 𝜌)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂) ∧ (𝜁 ∧ 𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) |
|
Theorem | syl332anc 1200 |
Syllogism combined with contraction. (Contributed by NM,
11-Mar-2012.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → 𝜒)
& ⊢ (𝜑 → 𝜃)
& ⊢ (𝜑 → 𝜏)
& ⊢ (𝜑 → 𝜂)
& ⊢ (𝜑 → 𝜁)
& ⊢ (𝜑 → 𝜎)
& ⊢ (𝜑 → 𝜌)
& ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁) ∧ (𝜎 ∧ 𝜌)) → 𝜇) ⇒ ⊢ (𝜑 → 𝜇) |