P. 13 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 1201-1300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	syl213anc 1201	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- (ph -> ps)   &   |- (ph -> ch)   &   |- (ph -> th)   &   |- (ph -> ta)   &   |- (ph -> et)   &   |- (ph -> ze)   &   |- (((ps /\ ch) /\ th /\ (ta /\ et /\ ze)) -> si)   =>   |- (ph -> si)
Theorem	syl231anc 1202	Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
|- (ph -> ps)   &   |- (ph -> ch)   &   |- (ph -> th)   &   |- (ph -> ta)   &   |- (ph -> et)   &   |- (ph -> ze)   &   |- (((ps /\ ch) /\ (th /\ ta /\ et) /\ ze) -> si)   =>   |- (ph -> si)
Theorem	syl312anc 1203	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
|- (ph -> ps)   &   |- (ph -> ch)   &   |- (ph -> th)   &   |- (ph -> ta)   &   |- (ph -> et)   &   |- (ph -> ze)   &   |- (((ps /\ ch /\ th) /\ ta /\ (et /\ ze)) -> si)   =>   |- (ph -> si)
Theorem	syl321anc 1204	Syllogism combined with contraction. (Contributed by NM, 11-Jul-2012.)
|- (ph -> ps)   &   |- (ph -> ch)   &   |- (ph -> th)   &   |- (ph -> ta)   &   |- (ph -> et)   &   |- (ph -> ze)   &   |- (((ps /\ ch /\ th) /\ (ta /\ et) /\ ze) -> si)   =>   |- (ph -> si)
Theorem	syl133anc 1205	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 1206	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 1207	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 1208	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 1209	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 1210	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 1211	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 1212	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 1213	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 1214	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 1215	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- (ph -> ps)   &   |- ((ps /\ ch /\ th) -> ta)   =>   |- ((ph /\ ch /\ th) -> ta)
Theorem	syl3an2 1216	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- (ph -> ch)   &   |- ((ps /\ ch /\ th) -> ta)   =>   |- ((ps /\ ph /\ th) -> ta)
Theorem	syl3an3 1217	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- (ph -> th)   &   |- ((ps /\ ch /\ th) -> ta)   =>   |- ((ps /\ ch /\ ph) -> ta)
Theorem	syl3an1b 1218	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- (ph <-> ps)   &   |- ((ps /\ ch /\ th) -> ta)   =>   |- ((ph /\ ch /\ th) -> ta)
Theorem	syl3an2b 1219	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- (ph <-> ch)   &   |- ((ps /\ ch /\ th) -> ta)   =>   |- ((ps /\ ph /\ th) -> ta)
Theorem	syl3an3b 1220	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- (ph <-> th)   &   |- ((ps /\ ch /\ th) -> ta)   =>   |- ((ps /\ ch /\ ph) -> ta)
Theorem	syl3an1br 1221	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- (ps <-> ph)   &   |- ((ps /\ ch /\ th) -> ta)   =>   |- ((ph /\ ch /\ th) -> ta)
Theorem	syl3an2br 1222	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- (ch <-> ph)   &   |- ((ps /\ ch /\ th) -> ta)   =>   |- ((ps /\ ph /\ th) -> ta)
Theorem	syl3an3br 1223	A syllogism inference. (Contributed by NM, 22-Aug-1995.)
|- (th <-> ph)   &   |- ((ps /\ ch /\ th) -> ta)   =>   |- ((ps /\ ch /\ ph) -> ta)
Theorem	syl3an 1224	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 1225	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 1226	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 1227	A syllogism inference. (Contributed by NM, 20-May-2007.)
|- ((ph /\ ps /\ ch) -> th)   &   |- ((ph /\ ps /\ th) -> ta)   =>   |- ((ph /\ ps /\ ch) -> ta)
Theorem	syld3an1 1228	A syllogism inference. (Contributed by NM, 7-Jul-2008.)
|- ((ch /\ ps /\ th) -> ph)   &   |- ((ph /\ ps /\ th) -> ta)   =>   |- ((ch /\ ps /\ th) -> ta)
Theorem	syld3an2 1229	A syllogism inference. (Contributed by NM, 20-May-2007.)
|- ((ph /\ ch /\ th) -> ps)   &   |- ((ph /\ ps /\ th) -> ta)   =>   |- ((ph /\ ch /\ th) -> ta)
Theorem	syl3anl1 1230	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- (ph -> ps)   &   |- (((ps /\ ch /\ th) /\ ta) -> et)   =>   |- (((ph /\ ch /\ th) /\ ta) -> et)
Theorem	syl3anl2 1231	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- (ph -> ch)   &   |- (((ps /\ ch /\ th) /\ ta) -> et)   =>   |- (((ps /\ ph /\ th) /\ ta) -> et)
Theorem	syl3anl3 1232	A syllogism inference. (Contributed by NM, 24-Feb-2005.)
|- (ph -> th)   &   |- (((ps /\ ch /\ th) /\ ta) -> et)   =>   |- (((ps /\ ch /\ ph) /\ ta) -> et)
Theorem	syl3anl 1233	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 1234	A syllogism inference. (Contributed by NM, 31-Jul-2007.)
|- (ph -> ps)   &   |- ((ch /\ (ps /\ th /\ ta)) -> et)   =>   |- ((ch /\ (ph /\ th /\ ta)) -> et)
Theorem	syl3anr2 1235	A syllogism inference. (Contributed by NM, 1-Aug-2007.)
|- (ph -> th)   &   |- ((ch /\ (ps /\ th /\ ta)) -> et)   =>   |- ((ch /\ (ps /\ ph /\ ta)) -> et)
Theorem	syl3anr3 1236	A syllogism inference. (Contributed by NM, 23-Aug-2007.)
|- (ph -> ta)   &   |- ((ch /\ (ps /\ th /\ ta)) -> et)   =>   |- ((ch /\ (ps /\ th /\ ph)) -> et)
Theorem	3impdi 1237	Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.)
|- (((ph /\ ps) /\ (ph /\ ch)) -> th)   =>   |- ((ph /\ ps /\ ch) -> th)
Theorem	3impdir 1238	Importation inference (undistribute conjunction). (Contributed by NM, 20-Aug-1995.)
|- (((ph /\ ps) /\ (ch /\ ps)) -> th)   =>   |- ((ph /\ ch /\ ps) -> th)
Theorem	3anidm12 1239	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
|- ((ph /\ ph /\ ps) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	3anidm13 1240	Inference from idempotent law for conjunction. (Contributed by NM, 7-Mar-2008.)
|- ((ph /\ ps /\ ph) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	3anidm23 1241	Inference from idempotent law for conjunction. (Contributed by NM, 1-Feb-2007.)
|- ((ph /\ ps /\ ps) -> ch)   =>   |- ((ph /\ ps) -> ch)
Theorem	3ori 1242	Infer implication from triple disjunction. (Contributed by NM, 26-Sep-2006.)
|- (ph \/ ps \/ ch)   =>   |- ((-. ph /\ -. ps) -> ch)
Theorem	3jao 1243	Disjunction of 3 antecedents. (Contributed by NM, 8-Apr-1994.)
|- (((ph -> ps) /\ (ch -> ps) /\ (th -> ps)) -> ((ph \/ ch \/ th) -> ps))
Theorem	3jaob 1244	Disjunction of 3 antecedents. (Contributed by NM, 13-Sep-2011.)
|- (((ph \/ ch \/ th) -> ps) <-> ((ph -> ps) /\ (ch -> ps) /\ (th -> ps)))
Theorem	3jaoi 1245	Disjunction of 3 antecedents (inference). (Contributed by NM, 12-Sep-1995.)
|- (ph -> ps)   &   |- (ch -> ps)   &   |- (th -> ps)   =>   |- ((ph \/ ch \/ th) -> ps)
Theorem	3jaod 1246	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 1247	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 1248	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	3jaao 1249	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	syl3an9b 1250	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 1251	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 1252	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 1253	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 1254	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 1255	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 1256	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> ((ps /\ th /\ ta) <-> (ch /\ th /\ ta)))
Theorem	3anbi2d 1257	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> ((th /\ ps /\ ta) <-> (th /\ ch /\ ta)))
Theorem	3anbi3d 1258	Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> ((th /\ ta /\ ps) <-> (th /\ ta /\ ch)))
Theorem	3anim123d 1259	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 1260	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 1261	Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995.)
|- (((ph /\ ps /\ ch) /\ (th /\ ta /\ et)) <-> ((ph /\ th) /\ (ps /\ ta) /\ (ch /\ et)))
Theorem	3an6 1262	Analog of an4 797 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 1263	Analog of or4 514 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.)
|- (((ph \/ ps) \/ (ch \/ th) \/ (ta \/ et)) <-> ((ph \/ ch \/ ta) \/ (ps \/ th \/ et)))
Theorem	mp3an1 1264	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
|- ph   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ps /\ ch) -> th)
Theorem	mp3an2 1265	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
|- ps   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ph /\ ch) -> th)
Theorem	mp3an3 1266	An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)
|- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	mp3an12 1267	An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
|- ph   &   |- ps   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- (ch -> th)
Theorem	mp3an13 1268	An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
|- ph   &   |- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- (ps -> th)
Theorem	mp3an23 1269	An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
|- ps   &   |- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- (ph -> th)
Theorem	mp3an1i 1270	An inference based on modus ponens. (Contributed by NM, 5-Jul-2005.)
|- ps   &   |- (ph -> ((ps /\ ch /\ th) -> ta))   =>   |- (ph -> ((ch /\ th) -> ta))
Theorem	mp3anl1 1271	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
|- ph   &   |- (((ph /\ ps /\ ch) /\ th) -> ta)   =>   |- (((ps /\ ch) /\ th) -> ta)
Theorem	mp3anl2 1272	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
|- ps   &   |- (((ph /\ ps /\ ch) /\ th) -> ta)   =>   |- (((ph /\ ch) /\ th) -> ta)
Theorem	mp3anl3 1273	An inference based on modus ponens. (Contributed by NM, 24-Feb-2005.)
|- ch   &   |- (((ph /\ ps /\ ch) /\ th) -> ta)   =>   |- (((ph /\ ps) /\ th) -> ta)
Theorem	mp3anr1 1274	An inference based on modus ponens. (Contributed by NM, 4-Nov-2006.)
|- ps   &   |- ((ph /\ (ps /\ ch /\ th)) -> ta)   =>   |- ((ph /\ (ch /\ th)) -> ta)
Theorem	mp3anr2 1275	An inference based on modus ponens. (Contributed by NM, 24-Nov-2006.)
|- ch   &   |- ((ph /\ (ps /\ ch /\ th)) -> ta)   =>   |- ((ph /\ (ps /\ th)) -> ta)
Theorem	mp3anr3 1276	An inference based on modus ponens. (Contributed by NM, 19-Oct-2007.)
|- th   &   |- ((ph /\ (ps /\ ch /\ th)) -> ta)   =>   |- ((ph /\ (ps /\ ch)) -> ta)
Theorem	mp3an 1277	An inference based on modus ponens. (Contributed by NM, 14-May-1999.)
|- ph   &   |- ps   &   |- ch   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- th
Theorem	mpd3an3 1278	An inference based on modus ponens. (Contributed by NM, 8-Nov-2007.)
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	mpd3an23 1279	An inference based on modus ponens. (Contributed by NM, 4-Dec-2006.)
|- (ph -> ps)   &   |- (ph -> ch)   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- (ph -> th)
Theorem	mp3and 1280	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	biimp3a 1281	Infer implication from a logical equivalence. Similar to biimpa 470. (Contributed by NM, 4-Sep-2005.)
|- ((ph /\ ps) -> (ch <-> th))   =>   |- ((ph /\ ps /\ ch) -> th)
Theorem	biimp3ar 1282	Infer implication from a logical equivalence. Similar to biimpar 471. (Contributed by NM, 2-Jan-2009.)
|- ((ph /\ ps) -> (ch <-> th))   =>   |- ((ph /\ ps /\ th) -> ch)
Theorem	3anandis 1283	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 1284	Inference that undistributes a triple conjunction in the antecedent. (Contributed by NM, 25-Jul-2006.)
|- (((ph /\ th) /\ (ps /\ th) /\ (ch /\ th)) -> ta)   =>   |- (((ph /\ ps /\ ch) /\ th) -> ta)
Theorem	ecase23d 1285	Deduction for elimination by cases. (Contributed by NM, 22-Apr-1994.)
|- (ph -> -. ch)   &   |- (ph -> -. th)   &   |- (ph -> (ps \/ ch \/ th))   =>   |- (ph -> ps)
Theorem	3ecase 1286	Inference for elimination by cases. (Contributed by NM, 13-Jul-2005.)
|- (-. ph -> th)   &   |- (-. ps -> th)   &   |- (-. ch -> th)   &   |- ((ph /\ ps /\ ch) -> th)   =>   |- th
1.2.9  Logical 'nand' (Sheffer stroke)
Syntax	wnan 1287	Extend wff definition to include alternative denial ('nand').
wff (ph -/\ ps)
Definition	df-nan 1288	Define incompatibility, or alternative denial ('not-and' or 'nand'). This is also called the Sheffer stroke, represented by a vertical bar, but we use a different symbol to avoid ambiguity with other uses of the vertical bar. In the second edition of Principia Mathematica (1927), Russell and Whitehead used the Sheffer stroke and suggested it as a replacement for the "or" and "not" operations of the first edition. However, in practice, "or" and "not" are more widely used. After we define the constant true T. (df-tru 1319) and the constant false F. (df-fal 1320), we will be able to prove these truth table values: (( T. -/\ T. ) <-> F. ) (trunantru 1354), (( T. -/\ F. ) <-> T. ) (trunanfal 1355), (( F. -/\ T. ) <-> T. ) (falnantru 1356), and (( F. -/\ F. ) <-> T. ) (falnanfal 1357). Contrast with /\ (df-an 360), \/ (df-or 359), -> (wi 4), and \/_ (df-xor 1305) . (Contributed by Jeff Hoffman, 19-Nov-2007.)
|- ((ph -/\ ps) <-> -. (ph /\ ps))
Theorem	nanan 1289	Write 'and' in terms of 'nand'. (Contributed by Mario Carneiro, 9-May-2015.)
|- ((ph /\ ps) <-> -. (ph -/\ ps))
Theorem	nancom 1290	The 'nand' operator commutes. (Contributed by Mario Carneiro, 9-May-2015.)
|- ((ph -/\ ps) <-> (ps -/\ ph))
Theorem	nannan 1291	Lemma for handling nested 'nand's. (Contributed by Jeff Hoffman, 19-Nov-2007.)
|- ((ph -/\ (ch -/\ ps)) <-> (ph -> (ch /\ ps)))
Theorem	nanim 1292	Show equivalence between implication and the Nicod version. To derive nic-dfim 1434, apply nanbi 1294. (Contributed by Jeff Hoffman, 19-Nov-2007.)
|- ((ph -> ps) <-> (ph -/\ (ps -/\ ps)))
Theorem	nannot 1293	Show equivalence between negation and the Nicod version. To derive nic-dfneg 1435, apply nanbi 1294. (Contributed by Jeff Hoffman, 19-Nov-2007.)
|- (-. ps <-> (ps -/\ ps))
Theorem	nanbi 1294	Show equivalence between the bidirectional and the Nicod version. (Contributed by Jeff Hoffman, 19-Nov-2007.)
|- ((ph <-> ps) <-> ((ph -/\ ps) -/\ ((ph -/\ ph) -/\ (ps -/\ ps))))
Theorem	nanbi1 1295	Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
|- ((ph <-> ps) -> ((ph -/\ ch) <-> (ps -/\ ch)))
Theorem	nanbi2 1296	Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
|- ((ph <-> ps) -> ((ch -/\ ph) <-> (ch -/\ ps)))
Theorem	nanbi12 1297	Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.)
|- (((ph <-> ps) /\ (ch <-> th)) -> ((ph -/\ ch) <-> (ps -/\ th)))
Theorem	nanbi1i 1298	Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
|- (ph <-> ps)   =>   |- ((ph -/\ ch) <-> (ps -/\ ch))
Theorem	nanbi2i 1299	Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.)
|- (ph <-> ps)   =>   |- ((ch -/\ ph) <-> (ch -/\ ps))
Theorem	nanbi12i 1300	Join two logical equivalences with anti-conjunction. (Contributed by SF, 2-Jan-2018.)
|- (ph <-> ps)   &   |- (ch <-> th)   =>   |- ((ph -/\ ch) <-> (ps -/\ th))