P. 5 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 401-500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	imor 401	Implication in terms of disjunction. Theorem *4.6 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.)
|- ((ph -> ps) <-> (-. ph \/ ps))
Theorem	imori 402	Infer disjunction from implication. (Contributed by NM, 12-Mar-2012.)
|- (ph -> ps)   =>   |- (-. ph \/ ps)
Theorem	imorri 403	Infer implication from disjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (-. ph \/ ps)   =>   |- (ph -> ps)
Theorem	exmid 404	Law of excluded middle, also called the principle of tertium non datur. Theorem *2.11 of [WhiteheadRussell] p. 101. It says that something is either true or not true; there are no in-between values of truth. This is an essential distinction of our classical logic and is not a theorem of intuitionistic logic. (Contributed by NM, 5-Aug-1993.)
|- (ph \/ -. ph)
Theorem	exmidd 405	Law of excluded middle in a context. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- (ph -> (ps \/ -. ps))
Theorem	pm2.1 406	Theorem *2.1 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
|- (-. ph \/ ph)
Theorem	pm2.13 407	Theorem *2.13 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.)
|- (ph \/ -. -. -. ph)
Theorem	pm4.62 408	Theorem *4.62 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
|- ((ph -> -. ps) <-> (-. ph \/ -. ps))
Theorem	pm4.66 409	Theorem *4.66 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
|- ((-. ph -> -. ps) <-> (ph \/ -. ps))
Theorem	pm4.63 410	Theorem *4.63 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
|- (-. (ph -> -. ps) <-> (ph /\ ps))
Theorem	imnan 411	Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.)
|- ((ph -> -. ps) <-> -. (ph /\ ps))
Theorem	imnani 412	Express implication in terms of conjunction. (Contributed by Mario Carneiro, 28-Sep-2015.)
|- -. (ph /\ ps)   =>   |- (ph -> -. ps)
Theorem	iman 413	Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2012.)
|- ((ph -> ps) <-> -. (ph /\ -. ps))
Theorem	annim 414	Express conjunction in terms of implication. (Contributed by NM, 2-Aug-1994.)
|- ((ph /\ -. ps) <-> -. (ph -> ps))
Theorem	pm4.61 415	Theorem *4.61 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
|- (-. (ph -> ps) <-> (ph /\ -. ps))
Theorem	pm4.65 416	Theorem *4.65 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
|- (-. (-. ph -> ps) <-> (-. ph /\ -. ps))
Theorem	pm4.67 417	Theorem *4.67 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
|- (-. (-. ph -> -. ps) <-> (-. ph /\ ps))
Theorem	imp 418	Importation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
|- (ph -> (ps -> ch))   =>   |- ((ph /\ ps) -> ch)
Theorem	impcom 419	Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
|- (ph -> (ps -> ch))   =>   |- ((ps /\ ph) -> ch)
Theorem	imp3a 420	Importation deduction. (Contributed by NM, 31-Mar-1994.)
|- (ph -> (ps -> (ch -> th)))   =>   |- (ph -> ((ps /\ ch) -> th))
Theorem	imp31 421	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> (ps -> (ch -> th)))   =>   |- (((ph /\ ps) /\ ch) -> th)
Theorem	imp32 422	An importation inference. (Contributed by NM, 26-Apr-1994.)
|- (ph -> (ps -> (ch -> th)))   =>   |- ((ph /\ (ps /\ ch)) -> th)
Theorem	ex 423	Exportation inference. (This theorem used to be labeled "exp" but was changed to "ex" so as not to conflict with the math token "exp", per the June 2006 Metamath spec change.) A translation of natural deduction rule -> I (-> introduction), see natded in set.mm. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
|- ((ph /\ ps) -> ch)   =>   |- (ph -> (ps -> ch))
Theorem	expcom 424	Exportation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
|- ((ph /\ ps) -> ch)   =>   |- (ps -> (ph -> ch))
Theorem	exp3a 425	Exportation deduction. (Contributed by NM, 20-Aug-1993.)
|- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> (ps -> (ch -> th)))
Theorem	expdimp 426	A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.)
|- (ph -> ((ps /\ ch) -> th))   =>   |- ((ph /\ ps) -> (ch -> th))
Theorem	impancom 427	Mixed importation/commutation inference. (Contributed by NM, 22-Jun-2013.)
|- ((ph /\ ps) -> (ch -> th))   =>   |- ((ph /\ ch) -> (ps -> th))
Theorem	con3and 428	Variant of con3d 125 with importation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
|- (ph -> (ps -> ch))   =>   |- ((ph /\ -. ch) -> -. ps)
Theorem	pm2.01da 429	Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ((ph /\ ps) -> -. ps)   =>   |- (ph -> -. ps)
Theorem	pm2.18da 430	Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- ((ph /\ -. ps) -> ps)   =>   |- (ph -> ps)
Theorem	pm3.3 431	Theorem *3.3 (Exp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
|- (((ph /\ ps) -> ch) -> (ph -> (ps -> ch)))
Theorem	pm3.31 432	Theorem *3.31 (Imp) of [WhiteheadRussell] p. 112. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
|- ((ph -> (ps -> ch)) -> ((ph /\ ps) -> ch))
Theorem	impexp 433	Import-export theorem. Part of Theorem *4.87 of [WhiteheadRussell] p. 122. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
|- (((ph /\ ps) -> ch) <-> (ph -> (ps -> ch)))
Theorem	pm3.2 434	Join antecedents with conjunction. Theorem *3.2 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.)
|- (ph -> (ps -> (ph /\ ps)))
Theorem	pm3.21 435	Join antecedents with conjunction. Theorem *3.21 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps -> (ps /\ ph)))
Theorem	pm3.22 436	Theorem *3.22 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
|- ((ph /\ ps) -> (ps /\ ph))
Theorem	ancom 437	Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.)
|- ((ph /\ ps) <-> (ps /\ ph))
Theorem	ancomd 438	Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.)
|- (ph -> (ps /\ ch))   =>   |- (ph -> (ch /\ ps))
Theorem	ancoms 439	Inference commuting conjunction in antecedent. (Contributed by NM, 21-Apr-1994.)
|- ((ph /\ ps) -> ch)   =>   |- ((ps /\ ph) -> ch)
Theorem	ancomsd 440	Deduction commuting conjunction in antecedent. (Contributed by NM, 12-Dec-2004.)
|- (ph -> ((ps /\ ch) -> th))   =>   |- (ph -> ((ch /\ ps) -> th))
Theorem	pm3.2i 441	Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.)
|- ph   &   |- ps   =>   |- (ph /\ ps)
Theorem	pm3.43i 442	Nested conjunction of antecedents. (Contributed by NM, 5-Aug-1993.)
|- ((ph -> ps) -> ((ph -> ch) -> (ph -> (ps /\ ch))))
Theorem	simpl 443	Elimination of a conjunct. Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
|- ((ph /\ ps) -> ph)
Theorem	simpli 444	Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)
|- (ph /\ ps)   =>   |- ph
Theorem	simpld 445	Deduction eliminating a conjunct. A translation of natural deduction rule /\ EL (/\ elimination left), see natded in set.mm. (Contributed by NM, 5-Aug-1993.)
|- (ph -> (ps /\ ch))   =>   |- (ph -> ps)
Theorem	simplbi 446	Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
|- (ph <-> (ps /\ ch))   =>   |- (ph -> ps)
Theorem	simpr 447	Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
|- ((ph /\ ps) -> ps)
Theorem	simpri 448	Inference eliminating a conjunct. (Contributed by NM, 15-Jun-1994.)
|- (ph /\ ps)   =>   |- ps
Theorem	simprd 449	Deduction eliminating a conjunct. (Contributed by NM, 5-Aug-1993.) A translation of natural deduction rule /\ ER (/\ elimination right), see natded in set.mm. (Proof shortened by Wolf Lammen, 3-Oct-2013.)
|- (ph -> (ps /\ ch))   =>   |- (ph -> ch)
Theorem	simprbi 450	Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)
|- (ph <-> (ps /\ ch))   =>   |- (ph -> ch)
Theorem	adantr 451	Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.)
|- (ph -> ps)   =>   |- ((ph /\ ch) -> ps)
Theorem	adantl 452	Inference adding a conjunct to the left of an antecedent. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
|- (ph -> ps)   =>   |- ((ch /\ ph) -> ps)
Theorem	adantld 453	Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)
|- (ph -> (ps -> ch))   =>   |- (ph -> ((th /\ ps) -> ch))
Theorem	adantrd 454	Deduction adding a conjunct to the right of an antecedent. (Contributed by NM, 4-May-1994.)
|- (ph -> (ps -> ch))   =>   |- (ph -> ((ps /\ th) -> ch))
Theorem	mpan9 455	Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- (ph -> ps)   &   |- (ch -> (ps -> th))   =>   |- ((ph /\ ch) -> th)
Theorem	syldan 456	A syllogism deduction with conjoined antecedents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)
|- ((ph /\ ps) -> ch)   &   |- ((ph /\ ch) -> th)   =>   |- ((ph /\ ps) -> th)
Theorem	sylan 457	A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
|- (ph -> ps)   &   |- ((ps /\ ch) -> th)   =>   |- ((ph /\ ch) -> th)
Theorem	sylanb 458	A syllogism inference. (Contributed by NM, 18-May-1994.)
|- (ph <-> ps)   &   |- ((ps /\ ch) -> th)   =>   |- ((ph /\ ch) -> th)
Theorem	sylanbr 459	A syllogism inference. (Contributed by NM, 18-May-1994.)
|- (ps <-> ph)   &   |- ((ps /\ ch) -> th)   =>   |- ((ph /\ ch) -> th)
Theorem	sylan2 460	A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)
|- (ph -> ch)   &   |- ((ps /\ ch) -> th)   =>   |- ((ps /\ ph) -> th)
Theorem	sylan2b 461	A syllogism inference. (Contributed by NM, 21-Apr-1994.)
|- (ph <-> ch)   &   |- ((ps /\ ch) -> th)   =>   |- ((ps /\ ph) -> th)
Theorem	sylan2br 462	A syllogism inference. (Contributed by NM, 21-Apr-1994.)
|- (ch <-> ph)   &   |- ((ps /\ ch) -> th)   =>   |- ((ps /\ ph) -> th)
Theorem	syl2an 463	A double syllogism inference. (Contributed by NM, 31-Jan-1997.)
|- (ph -> ps)   &   |- (ta -> ch)   &   |- ((ps /\ ch) -> th)   =>   |- ((ph /\ ta) -> th)
Theorem	syl2anr 464	A double syllogism inference. (Contributed by NM, 17-Sep-2013.)
|- (ph -> ps)   &   |- (ta -> ch)   &   |- ((ps /\ ch) -> th)   =>   |- ((ta /\ ph) -> th)
Theorem	syl2anb 465	A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
|- (ph <-> ps)   &   |- (ta <-> ch)   &   |- ((ps /\ ch) -> th)   =>   |- ((ph /\ ta) -> th)
Theorem	syl2anbr 466	A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
|- (ps <-> ph)   &   |- (ch <-> ta)   &   |- ((ps /\ ch) -> th)   =>   |- ((ph /\ ta) -> th)
Theorem	syland 467	A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
|- (ph -> (ps -> ch))   &   |- (ph -> ((ch /\ th) -> ta))   =>   |- (ph -> ((ps /\ th) -> ta))
Theorem	sylan2d 468	A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
|- (ph -> (ps -> ch))   &   |- (ph -> ((th /\ ch) -> ta))   =>   |- (ph -> ((th /\ ps) -> ta))
Theorem	syl2and 469	A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
|- (ph -> (ps -> ch))   &   |- (ph -> (th -> ta))   &   |- (ph -> ((ch /\ ta) -> et))   =>   |- (ph -> ((ps /\ th) -> et))
Theorem	biimpa 470	Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
|- (ph -> (ps <-> ch))   =>   |- ((ph /\ ps) -> ch)
Theorem	biimpar 471	Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
|- (ph -> (ps <-> ch))   =>   |- ((ph /\ ch) -> ps)
Theorem	biimpac 472	Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
|- (ph -> (ps <-> ch))   =>   |- ((ps /\ ph) -> ch)
Theorem	biimparc 473	Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
|- (ph -> (ps <-> ch))   =>   |- ((ch /\ ph) -> ps)
Theorem	ianor 474	Negated conjunction in terms of disjunction (De Morgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
|- (-. (ph /\ ps) <-> (-. ph \/ -. ps))
Theorem	anor 475	Conjunction in terms of disjunction (De Morgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Nov-2012.)
|- ((ph /\ ps) <-> -. (-. ph \/ -. ps))
Theorem	ioran 476	Negated disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- (-. (ph \/ ps) <-> (-. ph /\ -. ps))
Theorem	pm4.52 477	Theorem *4.52 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.)
|- ((ph /\ -. ps) <-> -. (-. ph \/ ps))
Theorem	pm4.53 478	Theorem *4.53 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
|- (-. (ph /\ -. ps) <-> (-. ph \/ ps))
Theorem	pm4.54 479	Theorem *4.54 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.)
|- ((-. ph /\ ps) <-> -. (ph \/ -. ps))
Theorem	pm4.55 480	Theorem *4.55 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
|- (-. (-. ph /\ ps) <-> (ph \/ -. ps))
Theorem	pm4.56 481	Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
|- ((-. ph /\ -. ps) <-> -. (ph \/ ps))
Theorem	oran 482	Disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- ((ph \/ ps) <-> -. (-. ph /\ -. ps))
Theorem	pm4.57 483	Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
|- (-. (-. ph /\ -. ps) <-> (ph \/ ps))
Theorem	pm3.1 484	Theorem *3.1 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
|- ((ph /\ ps) -> -. (-. ph \/ -. ps))
Theorem	pm3.11 485	Theorem *3.11 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
|- (-. (-. ph \/ -. ps) -> (ph /\ ps))
Theorem	pm3.12 486	Theorem *3.12 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
|- ((-. ph \/ -. ps) \/ (ph /\ ps))
Theorem	pm3.13 487	Theorem *3.13 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
|- (-. (ph /\ ps) -> (-. ph \/ -. ps))
Theorem	pm3.14 488	Theorem *3.14 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
|- ((-. ph \/ -. ps) -> -. (ph /\ ps))
Theorem	iba 489	Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.)
|- (ph -> (ps <-> (ps /\ ph)))
Theorem	ibar 490	Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.)
|- (ph -> (ps <-> (ph /\ ps)))
Theorem	biantru 491	A wff is equivalent to its conjunction with truth. (Contributed by NM, 5-Aug-1993.)
|- ph   =>   |- (ps <-> (ps /\ ph))
Theorem	biantrur 492	A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)
|- ph   =>   |- (ps <-> (ph /\ ps))
Theorem	biantrud 493	A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)
|- (ph -> ps)   =>   |- (ph -> (ch <-> (ch /\ ps)))
Theorem	biantrurd 494	A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)
|- (ph -> ps)   =>   |- (ph -> (ch <-> (ps /\ ch)))
Theorem	jaao 495	Inference conjoining and disjoining the antecedents of two implications. (Contributed by NM, 30-Sep-1999.)
|- (ph -> (ps -> ch))   &   |- (th -> (ta -> ch))   =>   |- ((ph /\ th) -> ((ps \/ ta) -> ch))
Theorem	jaoa 496	Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.)
|- (ph -> (ps -> ch))   &   |- (th -> (ta -> ch))   =>   |- ((ph \/ th) -> ((ps /\ ta) -> ch))
Theorem	pm3.44 497	Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
|- (((ps -> ph) /\ (ch -> ph)) -> ((ps \/ ch) -> ph))
Theorem	jao 498	Disjunction of antecedents. Compare Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 4-Apr-2013.)
|- ((ph -> ps) -> ((ch -> ps) -> ((ph \/ ch) -> ps)))
Theorem	pm1.2 499	Axiom *1.2 of [WhiteheadRussell] p. 96, which they call "Taut". (Contributed by NM, 3-Jan-2005.)
|- ((ph \/ ph) -> ph)
Theorem	oridm 500	Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.)
|- ((ph \/ ph) <-> ph)