P. 13 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1201-1300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	syl333anc 1201	A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> et )   &    |- ( ph -> ze )   &    |- ( ph -> si )   &    |- ( ph -> rh )   &    |- ( ph -> mu )   &    |- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et /\ ze ) /\ ( si /\ rh /\ mu ) ) -> la )   =>    |- ( ph -> la )
Theorem	syl3an1 1202	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph -> ps )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3an2 1203	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph -> ch )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ph /\ th ) -> ta )
Theorem	syl3an3 1204	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph -> th )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ch /\ ph ) -> ta )
Theorem	syl3an1b 1205	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph <-> ps )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3an2b 1206	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph <-> ch )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ph /\ th ) -> ta )
Theorem	syl3an3b 1207	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph <-> th )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ch /\ ph ) -> ta )
Theorem	syl3an1br 1208	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ps <-> ph )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3an2br 1209	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ch <-> ph )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ph /\ th ) -> ta )
Theorem	syl3an3br 1210	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( th <-> ph )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ch /\ ph ) -> ta )
Theorem	syl3an 1211	A triple syllogism inference. (Contributed by NM, 13-May-2004.)
|- ( ph -> ps )   &    |- ( ch -> th )   &    |- ( ta -> et )   &    |- ( ( ps /\ th /\ et ) -> ze )   =>    |- ( ( ph /\ ch /\ ta ) -> ze )
Theorem	syl3anb 1212	A triple syllogism inference. (Contributed by NM, 15-Oct-2005.)
|- ( ph <-> ps )   &    |- ( ch <-> th )   &    |- ( ta <-> et )   &    |- ( ( ps /\ th /\ et ) -> ze )   =>    |- ( ( ph /\ ch /\ ta ) -> ze )
Theorem	syl3anbr 1213	A triple syllogism inference. (Contributed by NM, 29-Dec-2011.)
|- ( ps <-> ph )   &    |- ( th <-> ch )   &    |- ( et <-> ta )   &    |- ( ( ps /\ th /\ et ) -> ze )   =>    |- ( ( ph /\ ch /\ ta ) -> ze )
Theorem	syld3an3 1214	A syllogism inference. (Contributed by NM, 20-May-2007.)
|- ( ( ph /\ ps /\ ch ) -> th )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ( ph /\ ps /\ ch ) -> ta )
Theorem	syld3an1 1215	A syllogism inference. (Contributed by NM, 7-Jul-2008.)
|- ( ( ch /\ ps /\ th ) -> ph )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ( ch /\ ps /\ th ) -> ta )
Theorem	syld3an2 1216	A syllogism inference. (Contributed by NM, 20-May-2007.)
|- ( ( ph /\ ch /\ th ) -> ps )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3anl1 1217	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> ps )   &    |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )   =>    |- ( ( ( ph /\ ch /\ th ) /\ ta ) -> et )
Theorem	syl3anl2 1218	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> ch )   &    |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )   =>    |- ( ( ( ps /\ ph /\ th ) /\ ta ) -> et )
Theorem	syl3anl3 1219	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> th )   &    |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )   =>    |- ( ( ( ps /\ ch /\ ph ) /\ ta ) -> et )
Theorem	syl3anl 1220	A triple syllogism inference. (Contributed by NM, 24-Dec-2006.)
|- ( ph -> ps )   &    |- ( ch -> th )   &    |- ( ta -> et )   &    |- ( ( ( ps /\ th /\ et ) /\ ze ) -> si )   =>    |- ( ( ( ph /\ ch /\ ta ) /\ ze ) -> si )
Theorem	syl3anr1 1221	A syllogism inference. (Contributed by NM, 31-Jul-2007.)
|- ( ph -> ps )   &    |- ( ( ch /\ ( ps /\ th /\ ta ) ) -> et )   =>    |- ( ( ch /\ ( ph /\ th /\ ta ) ) -> et )
Theorem	syl3anr2 1222	A syllogism inference. (Contributed by NM, 1-Aug-2007.)
|- ( ph -> th )   &    |- ( ( ch /\ ( ps /\ th /\ ta ) ) -> et )   =>    |- ( ( ch /\ ( ps /\ ph /\ ta ) ) -> et )
Theorem	syl3anr3 1223	A syllogism inference. (Contributed by NM, 23-Aug-2007.)
|- ( ph -> ta )   &    |- ( ( ch /\ ( ps /\ th /\ ta ) ) -> et )   =>    |- ( ( ch /\ ( ps /\ th /\ ph ) ) -> et )
Theorem	3impdi 1224	Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3impdir 1225	Importation inference (undistribute conjunction). (Contributed by NM, 20-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ ps ) ) -> th )   =>    |- ( ( ph /\ ch /\ ps ) -> th )
Theorem	3anidm12 1226	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
|- ( ( ph /\ ph /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	3anidm13 1227	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
|- ( ( ph /\ ps /\ ph ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	3anidm23 1228	Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
|- ( ( ph /\ ps /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	syl2an3an 1229	syl3an 1211 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( th -> ta )   &    |- ( ( ps /\ ch /\ ta ) -> et )   =>    |- ( ( ph /\ th ) -> et )
Theorem	syl2an23an 1230	Deduction related to syl3an 1211 with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ( th /\ ph ) -> ta )   &    |- ( ( ps /\ ch /\ ta ) -> et )   =>    |- ( ( th /\ ph ) -> et )
Theorem	3ori 1231	Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006.)
|- ( ph \/ ps \/ ch )   =>    |- ( ( -. ph /\ -. ps ) -> ch )
Theorem	3jao 1232	Disjunction of 3 antecedents. (Contributed by NM, 8-Apr-1994.)
|- ( ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) -> ( ( ph \/ ch \/ th ) -> ps ) )
Theorem	3jaob 1233	Disjunction of 3 antecedents. (Contributed by NM, 13-Sep-2011.)
|- ( ( ( ph \/ ch \/ th ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) )
Theorem	3jaoi 1234	Disjunction of 3 antecedents (inference). (Contributed by NM, 12-Sep-1995.)
|- ( ph -> ps )   &    |- ( ch -> ps )   &    |- ( th -> ps )   =>    |- ( ( ph \/ ch \/ th ) -> ps )
Theorem	3jaod 1235	Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( th -> ch ) )   &    |- ( ph -> ( ta -> ch ) )   =>    |- ( ph -> ( ( ps \/ th \/ ta ) -> ch ) )
Theorem	3jaoian 1236	Disjunction of 3 antecedents (inference). (Contributed by NM, 14-Oct-2005.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( th /\ ps ) -> ch )   &    |- ( ( ta /\ ps ) -> ch )   =>    |- ( ( ( ph \/ th \/ ta ) /\ ps ) -> ch )
Theorem	3jaodan 1237	Disjunction of 3 antecedents (deduction). (Contributed by NM, 14-Oct-2005.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ th ) -> ch )   &    |- ( ( ph /\ ta ) -> ch )   =>    |- ( ( ph /\ ( ps \/ th \/ ta ) ) -> ch )
Theorem	mpjao3dan 1238	Eliminate a 3-way disjunction in a deduction. (Contributed by Thierry Arnoux, 13-Apr-2018.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ th ) -> ch )   &    |- ( ( ph /\ ta ) -> ch )   &    |- ( ph -> ( ps \/ th \/ ta ) )   =>    |- ( ph -> ch )
Theorem	3jaao 1239	Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- ( ph -> ( ps -> ch ) )   &    |- ( th -> ( ta -> ch ) )   &    |- ( et -> ( ze -> ch ) )   =>    |- ( ( ph /\ th /\ et ) -> ( ( ps \/ ta \/ ze ) -> ch ) )
Theorem	3ianorr 1240	Triple disjunction implies negated triple conjunction. (Contributed by Jim Kingdon, 23-Dec-2018.)
|- ( ( -. ph \/ -. ps \/ -. ch ) -> -. ( ph /\ ps /\ ch ) )
Theorem	syl3an9b 1241	Nested syllogism inference conjoining 3 dissimilar antecedents. (Contributed by NM, 1-May-1995.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( th -> ( ch <-> ta ) )   &    |- ( et -> ( ta <-> ze ) )   =>    |- ( ( ph /\ th /\ et ) -> ( ps <-> ze ) )
Theorem	3orbi123d 1242	Deduction joining 3 equivalences to form equivalence of disjunctions. (Contributed by NM, 20-Apr-1994.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   &    |- ( ph -> ( et <-> ze ) )   =>    |- ( ph -> ( ( ps \/ th \/ et ) <-> ( ch \/ ta \/ ze ) ) )
Theorem	3anbi123d 1243	Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   &    |- ( ph -> ( et <-> ze ) )   =>    |- ( ph -> ( ( ps /\ th /\ et ) <-> ( ch /\ ta /\ ze ) ) )
Theorem	3anbi12d 1244	Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   =>    |- ( ph -> ( ( ps /\ th /\ et ) <-> ( ch /\ ta /\ et ) ) )
Theorem	3anbi13d 1245	Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   =>    |- ( ph -> ( ( ps /\ et /\ th ) <-> ( ch /\ et /\ ta ) ) )
Theorem	3anbi23d 1246	Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)
|- ( ph -> ( ps <-> ch ) )   &    |- ( ph -> ( th <-> ta ) )   =>    |- ( ph -> ( ( et /\ ps /\ th ) <-> ( et /\ ch /\ ta ) ) )
Theorem	3anbi1d 1247	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( ps /\ th /\ ta ) <-> ( ch /\ th /\ ta ) ) )
Theorem	3anbi2d 1248	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( th /\ ps /\ ta ) <-> ( th /\ ch /\ ta ) ) )
Theorem	3anbi3d 1249	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( th /\ ta /\ ps ) <-> ( th /\ ta /\ ch ) ) )
Theorem	3anim123d 1250	Deduction joining 3 implications to form implication of conjunctions. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( th -> ta ) )   &    |- ( ph -> ( et -> ze ) )   =>    |- ( ph -> ( ( ps /\ th /\ et ) -> ( ch /\ ta /\ ze ) ) )
Theorem	3orim123d 1251	Deduction joining 3 implications to form implication of disjunctions. (Contributed by NM, 4-Apr-1997.)
|- ( ph -> ( ps -> ch ) )   &    |- ( ph -> ( th -> ta ) )   &    |- ( ph -> ( et -> ze ) )   =>    |- ( ph -> ( ( ps \/ th \/ et ) -> ( ch \/ ta \/ ze ) ) )
Theorem	an6 1252	Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995.)
|- ( ( ( ph /\ ps /\ ch ) /\ ( th /\ ta /\ et ) ) <-> ( ( ph /\ th ) /\ ( ps /\ ta ) /\ ( ch /\ et ) ) )
Theorem	3an6 1253	Analog of an4 550 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) /\ ( ta /\ et ) ) <-> ( ( ph /\ ch /\ ta ) /\ ( ps /\ th /\ et ) ) )
Theorem	3or6 1254	Analog of or4 720 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.)
|- ( ( ( ph \/ ps ) \/ ( ch \/ th ) \/ ( ta \/ et ) ) <-> ( ( ph \/ ch \/ ta ) \/ ( ps \/ th \/ et ) ) )
Theorem	mp3an1 1255	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
|- ph   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ps /\ ch ) -> th )
Theorem	mp3an2 1256	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
|- ps   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ch ) -> th )
Theorem	mp3an3 1257	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
|- ch   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	mp3an12 1258	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
|- ph   &    |- ps   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ch -> th )
Theorem	mp3an13 1259	An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
|- ph   &    |- ch   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ps -> th )
Theorem	mp3an23 1260	An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
|- ps   &    |- ch   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	mp3an1i 1261	An inference based on modus ponens. (Contributed by NM, 5-Jul-2005.)
|- ps   &    |- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )   =>    |- ( ph -> ( ( ch /\ th ) -> ta ) )
Theorem	mp3anl1 1262	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
|- ph   &    |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ps /\ ch ) /\ th ) -> ta )
Theorem	mp3anl2 1263	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
|- ps   &    |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ th ) -> ta )
Theorem	mp3anl3 1264	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
|- ch   &    |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ph /\ ps ) /\ th ) -> ta )
Theorem	mp3anr1 1265	An inference based on modus ponens. (Contributed by NM, 4-Nov-2006.)
|- ps   &    |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )   =>    |- ( ( ph /\ ( ch /\ th ) ) -> ta )
Theorem	mp3anr2 1266	An inference based on modus ponens. (Contributed by NM, 24-Nov-2006.)
|- ch   &    |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )   =>    |- ( ( ph /\ ( ps /\ th ) ) -> ta )
Theorem	mp3anr3 1267	An inference based on modus ponens. (Contributed by NM, 19-Oct-2007.)
|- th   &    |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> ta )
Theorem	mp3an 1268	An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
|- ph   &    |- ps   &    |- ch   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- th
Theorem	mpd3an3 1269	An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	mpd3an23 1270	An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	mp3and 1271	A deduction based on modus ponens. (Contributed by Mario Carneiro, 24-Dec-2016.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )   =>    |- ( ph -> ta )
Theorem	mp3an12i 1272	mp3an 1268 with antecedents in standard conjunction form and with one hypothesis an implication. (Contributed by Alan Sare, 28-Aug-2016.)
|- ph   &    |- ps   &    |- ( ch -> th )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ch -> ta )
Theorem	mp3an2i 1273	mp3an 1268 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)
|- ph   &    |- ( ps -> ch )   &    |- ( ps -> th )   &    |- ( ( ph /\ ch /\ th ) -> ta )   =>    |- ( ps -> ta )
Theorem	mp3an3an 1274	mp3an 1268 with antecedents in standard conjunction form and with two hypotheses which are implications. (Contributed by Alan Sare, 28-Aug-2016.)
|- ph   &    |- ( ps -> ch )   &    |- ( th -> ta )   &    |- ( ( ph /\ ch /\ ta ) -> et )   =>    |- ( ( ps /\ th ) -> et )
Theorem	mp3an2ani 1275	An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017.)
|- ph   &    |- ( ps -> ch )   &    |- ( ( ps /\ th ) -> ta )   &    |- ( ( ph /\ ch /\ ta ) -> et )   =>    |- ( ( ps /\ th ) -> et )
Theorem	biimp3a 1276	Infer implication from a logical equivalence. Similar to biimpa 290. (Contributed by NM, 4-Sep-2005.)
|- ( ( ph /\ ps ) -> ( ch <-> th ) )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	biimp3ar 1277	Infer implication from a logical equivalence. Similar to biimpar 291. (Contributed by NM, 2-Jan-2009.)
|- ( ( ph /\ ps ) -> ( ch <-> th ) )   =>    |- ( ( ph /\ ps /\ th ) -> ch )
Theorem	3anandis 1278	Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 18-Apr-2007.)
|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) /\ ( ph /\ th ) ) -> ta )   =>    |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )
Theorem	3anandirs 1279	Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 25-Jul-2006.) (Revised by NM, 18-Apr-2007.)
|- ( ( ( ph /\ th ) /\ ( ps /\ th ) /\ ( ch /\ th ) ) -> ta )   =>    |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )
Theorem	ecased 1280	Deduction form of disjunctive syllogism. (Contributed by Jim Kingdon, 9-Dec-2017.)
|- ( ph -> -. ch )   &    |- ( ph -> ( ps \/ ch ) )   =>    |- ( ph -> ps )
Theorem	ecase23d 1281	Variation of ecased 1280 with three disjuncts instead of two. (Contributed by NM, 22-Apr-1994.) (Revised by Jim Kingdon, 9-Dec-2017.)
|- ( ph -> -. ch )   &    |- ( ph -> -. th )   &    |- ( ph -> ( ps \/ ch \/ th ) )   =>    |- ( ph -> ps )
1.2.13  True and false constants
1.2.13.1  Universal quantifier for use by df-tru Even though it isn't ordinarily part of propositional calculus, the universal quantifier A. is introduced here so that the soundness of definition df-tru 1287 can be checked by the same algorithm that is used for predicate calculus. Its first real use is in axiom ax-5 1376 in the predicate calculus section below. For those who want propositional calculus to be self-contained i.e. to use wff variables only, the alternate definition dftru2 1292 may be adopted and this subsection moved down to the start of the subsection with wex 1421 below. However, the use of dftru2 1292 as a definition requires a more elaborate definition checking algorithm that we prefer to avoid.
Syntax	wal 1282	Extend wff definition to include the universal quantifier ('for all'). A. x ph is read " ph (phi) is true for all x." Typically, in its final application ph would be replaced with a wff containing a (free) occurrence of the variable x, for example x = y. In a universe with a finite number of objects, "for all" is equivalent to a big conjunction (AND) with one wff for each possible case of x. When the universe is infinite (as with set theory), such a propositional-calculus equivalent is not possible because an infinitely long formula has no meaning, but conceptually the idea is the same.
wff A. x ph
1.2.13.2  Equality predicate for use by df-tru Even though it isn't ordinarily part of propositional calculus, the equality predicate = is introduced here so that the soundness of definition df-tru 1287 can be checked by the same algorithm as is used for predicate calculus. Its first real use is in axiom ax-8 1435 in the predicate calculus section below. For those who want propositional calculus to be self-contained i.e. to use wff variables only, the alternate definition dftru2 1292 may be adopted and this subsection moved down to just above weq 1432 below. However, the use of dftru2 1292 as a definition requires a more elaborate definition checking algorithm that we prefer to avoid.
Syntax	cv 1283	This syntax construction states that a variable x, which has been declared to be a setvar variable by $f statement vx, is also a class expression. This can be justified informally as follows. We know that the class builder { y | y e. x } is a class by cab 2067. Since (when y is distinct from x) we have x = { y | y e. x } by cvjust 2076, we can argue that the syntax " class x " can be viewed as an abbreviation for " class { y | y e. x }". See the discussion under the definition of class in [Jech] p. 4 showing that "Every set can be considered to be a class." While it is tempting and perhaps occasionally useful to view cv 1283 as a "type conversion" from a setvar variable to a class variable, keep in mind that cv 1283 is intrinsically no different from any other class-building syntax such as cab 2067, cun 2971, or c0 3251. For a general discussion of the theory of classes and the role of cv 1283, see http://us.metamath.org/mpeuni/mmset.html#class. (The description above applies to set theory, not predicate calculus. The purpose of introducing class x here, and not in set theory where it belongs, is to allow us to express i.e. "prove" the weq 1432 of predicate calculus from the wceq 1284 of set theory, so that we don't overload the = connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers.)
class x
Syntax	wceq 1284	Extend wff definition to include class equality. For a general discussion of the theory of classes, see http://us.metamath.org/mpeuni/mmset.html#class. (The purpose of introducing wff A = B here, and not in set theory where it belongs, is to allow us to express i.e. "prove" the weq 1432 of predicate calculus in terms of the wceq 1284 of set theory, so that we don't "overload" the = connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers. For example, some parsers - although not the Metamath program - stumble on the fact that the = in x = y could be the = of either weq 1432 or wceq 1284, although mathematically it makes no difference. The class variables A and B are introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus. See df-cleq 2074 for more information on the set theory usage of wceq 1284.)
wff A = B
1.2.13.3  Define the true and false constants
Syntax	wtru 1285	T. is a wff.
wff T.
Theorem	trujust 1286	Soundness justification theorem for df-tru 1287. (Contributed by Mario Carneiro, 17-Nov-2013.) (Revised by NM, 11-Jul-2019.)
|- ( ( A. x x = x -> A. x x = x ) <-> ( A. y y = y -> A. y y = y ) )
Definition	df-tru 1287	Definition of the truth value "true", or "verum", denoted by T.. This is a tautology, as proved by tru 1288. In this definition, an instance of id 19 is used as the definiens, although any tautology, such as an axiom, can be used in its place. This particular id 19 instance was chosen so this definition can be checked by the same algorithm that is used for predicate calculus. This definition should be referenced directly only by tru 1288, and other proofs should depend on tru 1288 (directly or indirectly) instead of this definition, since there are many alternate ways to define T.. (Contributed by Anthony Hart, 13-Oct-2010.) (Revised by NM, 11-Jul-2019.) (New usage is discouraged.)
|- ( T. <-> ( A. x x = x -> A. x x = x ) )
Theorem	tru 1288	The truth value T. is provable. (Contributed by Anthony Hart, 13-Oct-2010.)
|- T.
Syntax	wfal 1289	F. is a wff.
wff F.
Definition	df-fal 1290	Definition of the truth value "false", or "falsum", denoted by F.. See also df-tru 1287. (Contributed by Anthony Hart, 22-Oct-2010.)
|- ( F. <-> -. T. )
Theorem	fal 1291	The truth value F. is refutable. (Contributed by Anthony Hart, 22-Oct-2010.) (Proof shortened by Mel L. O'Cat, 11-Mar-2012.)
|- -. F.
Theorem	dftru2 1292	An alternate definition of "true". (Contributed by Anthony Hart, 13-Oct-2010.) (Revised by BJ, 12-Jul-2019.) (New usage is discouraged.)
|- ( T. <-> ( ph -> ph ) )
Theorem	trud 1293	Eliminate T. as an antecedent. A proposition implied by T. is true. (Contributed by Mario Carneiro, 13-Mar-2014.)
|- ( T. -> ph )   =>    |- ph
Theorem	tbtru 1294	A proposition is equivalent to itself being equivalent to T.. (Contributed by Anthony Hart, 14-Aug-2011.)
|- ( ph <-> ( ph <-> T. ) )
Theorem	nbfal 1295	The negation of a proposition is equivalent to itself being equivalent to F.. (Contributed by Anthony Hart, 14-Aug-2011.)
|- ( -. ph <-> ( ph <-> F. ) )
Theorem	bitru 1296	A theorem is equivalent to truth. (Contributed by Mario Carneiro, 9-May-2015.)
|- ph   =>    |- ( ph <-> T. )
Theorem	bifal 1297	A contradiction is equivalent to falsehood. (Contributed by Mario Carneiro, 9-May-2015.)
|- -. ph   =>    |- ( ph <-> F. )
Theorem	falim 1298	The truth value F. implies anything. Also called the principle of explosion, or "ex falso quodlibet". (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)
|- ( F. -> ph )
Theorem	falimd 1299	The truth value F. implies anything. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ( ( ph /\ F. ) -> ps )
Theorem	a1tru 1300	Anything implies T.. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Anthony Hart, 1-Aug-2011.)
|- ( ph -> T. )