P. 14 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1301-1400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	syl133anc 1301	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> et )   &    |- ( ph -> ze )   &    |- ( ph -> si )   &    |- ( ( ps /\ ( ch /\ th /\ ta ) /\ ( et /\ ze /\ si ) ) -> rh )   =>    |- ( ph -> rh )
Theorem	syl313anc 1302	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> et )   &    |- ( ph -> ze )   &    |- ( ph -> si )   &    |- ( ( ( ps /\ ch /\ th ) /\ ta /\ ( et /\ ze /\ si ) ) -> rh )   =>    |- ( ph -> rh )
Theorem	syl331anc 1303	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> et )   &    |- ( ph -> ze )   &    |- ( ph -> si )   &    |- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et /\ ze ) /\ si ) -> rh )   =>    |- ( ph -> rh )
Theorem	syl223anc 1304	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> et )   &    |- ( ph -> ze )   &    |- ( ph -> si )   &    |- ( ( ( ps /\ ch ) /\ ( th /\ ta ) /\ ( et /\ ze /\ si ) ) -> rh )   =>    |- ( ph -> rh )
Theorem	syl232anc 1305	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> et )   &    |- ( ph -> ze )   &    |- ( ph -> si )   &    |- ( ( ( ps /\ ch ) /\ ( th /\ ta /\ et ) /\ ( ze /\ si ) ) -> rh )   =>    |- ( ph -> rh )
Theorem	syl322anc 1306	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> et )   &    |- ( ph -> ze )   &    |- ( ph -> si )   &    |- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et ) /\ ( ze /\ si ) ) -> rh )   =>    |- ( ph -> rh )
Theorem	syl233anc 1307	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> et )   &    |- ( ph -> ze )   &    |- ( ph -> si )   &    |- ( ph -> rh )   &    |- ( ( ( ps /\ ch ) /\ ( th /\ ta /\ et ) /\ ( ze /\ si /\ rh ) ) -> mu )   =>    |- ( ph -> mu )
Theorem	syl323anc 1308	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> et )   &    |- ( ph -> ze )   &    |- ( ph -> si )   &    |- ( ph -> rh )   &    |- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et ) /\ ( ze /\ si /\ rh ) ) -> mu )   =>    |- ( ph -> mu )
Theorem	syl332anc 1309	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ph -> th )   &    |- ( ph -> ta )   &    |- ( ph -> et )   &    |- ( ph -> ze )   &    |- ( ph -> si )   &    |- ( ph -> rh )   &    |- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et /\ ze ) /\ ( si /\ rh ) ) -> mu )   =>    |- ( ph -> mu )
Theorem	syl333anc 1310	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 1311	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph -> ps )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3an2 1312	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph -> ch )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ph /\ th ) -> ta )
Theorem	syl3an3 1313	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph -> th )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ch /\ ph ) -> ta )
Theorem	syl3an1b 1314	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph <-> ps )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3an2b 1315	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph <-> ch )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ph /\ th ) -> ta )
Theorem	syl3an3b 1316	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ph <-> th )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ch /\ ph ) -> ta )
Theorem	syl3an1br 1317	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ps <-> ph )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3an2br 1318	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( ch <-> ph )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ph /\ th ) -> ta )
Theorem	syl3an3br 1319	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- ( th <-> ph )   &    |- ( ( ps /\ ch /\ th ) -> ta )   =>    |- ( ( ps /\ ch /\ ph ) -> ta )
Theorem	syl3an 1320	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 1321	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 1322	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 1323	A syllogism inference. (Contributed by NM, 20-May-2007.)
|- ( ( ph /\ ps /\ ch ) -> th )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ( ph /\ ps /\ ch ) -> ta )
Theorem	syld3an1 1324	A syllogism inference. (Contributed by NM, 7-Jul-2008.)
|- ( ( ch /\ ps /\ th ) -> ph )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ( ch /\ ps /\ th ) -> ta )
Theorem	syld3an2 1325	A syllogism inference. (Contributed by NM, 20-May-2007.)
|- ( ( ph /\ ch /\ th ) -> ps )   &    |- ( ( ph /\ ps /\ th ) -> ta )   =>    |- ( ( ph /\ ch /\ th ) -> ta )
Theorem	syl3anl1 1326	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> ps )   &    |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )   =>    |- ( ( ( ph /\ ch /\ th ) /\ ta ) -> et )
Theorem	syl3anl2 1327	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> ch )   &    |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )   =>    |- ( ( ( ps /\ ph /\ th ) /\ ta ) -> et )
Theorem	syl3anl3 1328	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- ( ph -> th )   &    |- ( ( ( ps /\ ch /\ th ) /\ ta ) -> et )   =>    |- ( ( ( ps /\ ch /\ ph ) /\ ta ) -> et )
Theorem	syl3anl 1329	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 1330	A syllogism inference. (Contributed by NM, 31-Jul-2007.)
|- ( ph -> ps )   &    |- ( ( ch /\ ( ps /\ th /\ ta ) ) -> et )   =>    |- ( ( ch /\ ( ph /\ th /\ ta ) ) -> et )
Theorem	syl3anr2 1331	A syllogism inference. (Contributed by NM, 1-Aug-2007.)
|- ( ph -> th )   &    |- ( ( ch /\ ( ps /\ th /\ ta ) ) -> et )   =>    |- ( ( ch /\ ( ps /\ ph /\ ta ) ) -> et )
Theorem	syl3anr3 1332	A syllogism inference. (Contributed by NM, 23-Aug-2007.)
|- ( ph -> ta )   &    |- ( ( ch /\ ( ps /\ th /\ ta ) ) -> et )   =>    |- ( ( ch /\ ( ps /\ th /\ ph ) ) -> et )
Theorem	syldbl2 1333	Stacked hypotheseis implies goal. (Contributed by Stanislas Polu, 9-Mar-2020.)
|- ( ( ph /\ ps ) -> ( ps -> th ) )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	3impdi 1334	Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ph /\ ch ) ) -> th )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	3impdir 1335	Importation inference (undistribute conjunction). (Contributed by NM, 20-Aug-1995.)
|- ( ( ( ph /\ ps ) /\ ( ch /\ ps ) ) -> th )   =>    |- ( ( ph /\ ch /\ ps ) -> th )
Theorem	3anidm12 1336	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
|- ( ( ph /\ ph /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	3anidm13 1337	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
|- ( ( ph /\ ps /\ ph ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	3anidm23 1338	Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
|- ( ( ph /\ ps /\ ps ) -> ch )   =>    |- ( ( ph /\ ps ) -> ch )
Theorem	syl2an3an 1339	syl3an 1320 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 1340	Deduction related to syl3an 1320 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 1341	Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006.)
|- ( ph \/ ps \/ ch )   =>    |- ( ( -. ph /\ -. ps ) -> ch )
Theorem	3jao 1342	Disjunction of 3 antecedents. (Contributed by NM, 8-Apr-1994.)
|- ( ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) -> ( ( ph \/ ch \/ th ) -> ps ) )
Theorem	3jaob 1343	Disjunction of 3 antecedents. (Contributed by NM, 13-Sep-2011.)
|- ( ( ( ph \/ ch \/ th ) -> ps ) <-> ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) )
Theorem	3jaoi 1344	Disjunction of 3 antecedents (inference). (Contributed by NM, 12-Sep-1995.)
|- ( ph -> ps )   &    |- ( ch -> ps )   &    |- ( th -> ps )   =>    |- ( ( ph \/ ch \/ th ) -> ps )
Theorem	3jaod 1345	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 1346	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 1347	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 1348	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 1349	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 1350	Triple disjunction implies negated triple conjunction. (Contributed by Jim Kingdon, 23-Dec-2018.)
|- ( ( -. ph \/ -. ps \/ -. ch ) -> -. ( ph /\ ps /\ ch ) )
Theorem	syl3an9b 1351	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 1352	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 1353	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 1354	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 1355	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 1356	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 1357	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( ps /\ th /\ ta ) <-> ( ch /\ th /\ ta ) ) )
Theorem	3anbi2d 1358	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( th /\ ps /\ ta ) <-> ( th /\ ch /\ ta ) ) )
Theorem	3anbi3d 1359	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( ( th /\ ta /\ ps ) <-> ( th /\ ta /\ ch ) ) )
Theorem	3anim123d 1360	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 1361	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 1362	Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995.)
|- ( ( ( ph /\ ps /\ ch ) /\ ( th /\ ta /\ et ) ) <-> ( ( ph /\ th ) /\ ( ps /\ ta ) /\ ( ch /\ et ) ) )
Theorem	3an6 1363	Analog of an4 592 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 1364	Analog of or4 783 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.)
|- ( ( ( ph \/ ps ) \/ ( ch \/ th ) \/ ( ta \/ et ) ) <-> ( ( ph \/ ch \/ ta ) \/ ( ps \/ th \/ et ) ) )
Theorem	mp3an1 1365	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
|- ph   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ps /\ ch ) -> th )
Theorem	mp3an2 1366	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
|- ps   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ch ) -> th )
Theorem	mp3an3 1367	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
|- ch   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	mp3an12 1368	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
|- ph   &    |- ps   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ch -> th )
Theorem	mp3an13 1369	An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
|- ph   &    |- ch   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ps -> th )
Theorem	mp3an23 1370	An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
|- ps   &    |- ch   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	mp3an1i 1371	An inference based on modus ponens. (Contributed by NM, 5-Jul-2005.)
|- ps   &    |- ( ph -> ( ( ps /\ ch /\ th ) -> ta ) )   =>    |- ( ph -> ( ( ch /\ th ) -> ta ) )
Theorem	mp3anl1 1372	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
|- ph   &    |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ps /\ ch ) /\ th ) -> ta )
Theorem	mp3anl2 1373	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
|- ps   &    |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ph /\ ch ) /\ th ) -> ta )
Theorem	mp3anl3 1374	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
|- ch   &    |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ta )   =>    |- ( ( ( ph /\ ps ) /\ th ) -> ta )
Theorem	mp3anr1 1375	An inference based on modus ponens. (Contributed by NM, 4-Nov-2006.)
|- ps   &    |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )   =>    |- ( ( ph /\ ( ch /\ th ) ) -> ta )
Theorem	mp3anr2 1376	An inference based on modus ponens. (Contributed by NM, 24-Nov-2006.)
|- ch   &    |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )   =>    |- ( ( ph /\ ( ps /\ th ) ) -> ta )
Theorem	mp3anr3 1377	An inference based on modus ponens. (Contributed by NM, 19-Oct-2007.)
|- th   &    |- ( ( ph /\ ( ps /\ ch /\ th ) ) -> ta )   =>    |- ( ( ph /\ ( ps /\ ch ) ) -> ta )
Theorem	mp3an 1378	An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
|- ph   &    |- ps   &    |- ch   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- th
Theorem	mpd3an3 1379	An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
|- ( ( ph /\ ps ) -> ch )   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ( ph /\ ps ) -> th )
Theorem	mpd3an23 1380	An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.)
|- ( ph -> ps )   &    |- ( ph -> ch )   &    |- ( ( ph /\ ps /\ ch ) -> th )   =>    |- ( ph -> th )
Theorem	mp3and 1381	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 1382	mp3an 1378 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 1383	mp3an 1378 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 1384	mp3an 1378 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 1385	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 1386	Infer implication from a logical equivalence. Similar to biimpa 296. (Contributed by NM, 4-Sep-2005.)
|- ( ( ph /\ ps ) -> ( ch <-> th ) )   =>    |- ( ( ph /\ ps /\ ch ) -> th )
Theorem	biimp3ar 1387	Infer implication from a logical equivalence. Similar to biimpar 297. (Contributed by NM, 2-Jan-2009.)
|- ( ( ph /\ ps ) -> ( ch <-> th ) )   =>    |- ( ( ph /\ ps /\ th ) -> ch )
Theorem	3anandis 1388	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 1389	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 1390	Deduction form of disjunctive syllogism. (Contributed by Jim Kingdon, 9-Dec-2017.)
|- ( ph -> -. ch )   &    |- ( ph -> ( ps \/ ch ) )   =>    |- ( ph -> ps )
Theorem	ecase23d 1391	Variation of ecased 1390 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 )
Theorem	ecase2d 1392	Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Sep-2024.)
|- ( ph -> ps )   &    |- ( ph -> -. ( ps /\ ch ) )   &    |- ( ph -> -. ( ps /\ th ) )   &    |- ( ph -> ( ta \/ ( ch \/ th ) ) )   =>    |- ( ph -> ta )
Theorem	3bior1fd 1393	A disjunction is equivalent to a threefold disjunction with single falsehood, analogous to biorf 756. (Contributed by Alexander van der Vekens, 8-Sep-2017.)
|- ( ph -> -. th )   =>    |- ( ph -> ( ( ch \/ ps ) <-> ( th \/ ch \/ ps ) ) )
Theorem	3bior1fand 1394	A disjunction is equivalent to a threefold disjunction with single falsehood of a conjunction. (Contributed by Alexander van der Vekens, 8-Sep-2017.)
|- ( ph -> -. th )   =>    |- ( ph -> ( ( ch \/ ps ) <-> ( ( th /\ ta ) \/ ch \/ ps ) ) )
Theorem	3bior2fd 1395	A wff is equivalent to its threefold disjunction with double falsehood, analogous to biorf 756. (Contributed by Alexander van der Vekens, 8-Sep-2017.)
|- ( ph -> -. th )   &    |- ( ph -> -. ch )   =>    |- ( ph -> ( ps <-> ( th \/ ch \/ ps ) ) )
Theorem	3biant1d 1396	A conjunction is equivalent to a threefold conjunction with single truth, analogous to biantrud 304. (Contributed by Alexander van der Vekens, 26-Sep-2017.)
|- ( ph -> th )   =>    |- ( ph -> ( ( ch /\ ps ) <-> ( th /\ ch /\ ps ) ) )
Theorem	intn3an1d 1397	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. ( ps /\ ch /\ th ) )
Theorem	intn3an2d 1398	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. ( ch /\ ps /\ th ) )
Theorem	intn3an3d 1399	Introduction of a triple conjunct inside a contradiction. (Contributed by FL, 27-Dec-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. ( ch /\ th /\ ps ) )
1.2.13  True and false constants
1.2.13.1  Universal quantifier for use by df-tru Even though it is not ordinarily part of propositional calculus, the universal quantifier A. is introduced here so that the soundness of Definition df-tru 1405 can be checked by the same algorithm that is used for predicate calculus. Its first real use is in Axiom ax-5 1500 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 1410 may be adopted and this subsection moved down to the start of the subsection with wex 1545 below. However, the use of dftru2 1410 as a definition requires a more elaborate definition checking algorithm that we prefer to avoid.
Syntax	wal 1400	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