Ghilbert theorems

idi(Note: This inference rule and the next one, a1ii, will normally never appear in a completed proof

a1ii(Note: This inference rule and the previous one, idi, will normally never appear in a completed proof.) This is a technical inference to assist proof development

Propositional calculus

Logical implication

mp2A double modus ponens inference

mp2bA double modus ponens inference

a1iInference introducing an antecedent

2a1iInference introducing two antecedents

ax1wWeakening of ax-1

mp1iInference detaching an antecedent and introducing a new one

a2iInference distributing an antecedent

mpdA modus ponens deduction

imim2iInference adding common antecedents in an implication

sylAn inference version of the transitive laws for implication imim2 and imim1 (and imim1i and imim2i ), which Russell and Whitehead call "the principle of the syllogism ..

3sylInference chaining two syllogisms syl

4sylInference chaining three syllogisms syl

mpiA nested modus ponens inference

mpisylA syllogism combined with a modus ponens inference

idPrinciple of identity

idALTAlternate proof of id

iddPrinciple of identity id with antecedent

a1dDeduction introducing an embedded antecedent

2a1dDeduction introducing two antecedents

a1i13Add two antecedents to a wff

2a1A double form of ax-1

a2dDeduction distributing an embedded antecedent

sylcomSyllogism inference with commutation of antecedents

syl5comSyllogism inference with commuted antecedents

com12Inference that swaps (commutes) antecedents in an implication

syl11A syllogism inference

syl5A syllogism rule of inference

syl6A syllogism rule of inference

syl56Combine syl5 and syl6

syl6comSyllogism inference with commuted antecedents

mpcomModus ponens inference with commutation of antecedents

syliSyllogism inference with common nested antecedent

syl2imReplace two antecedents

syl2imcA commuted version of syl2im

pm2.27This theorem, sometimes called "Assertion" or "Pon" (for "ponens"), can be thought of as a closed form of modus ponens ax-mp

mpddA nested modus ponens deduction

mpidA nested modus ponens deduction

mpdiA nested modus ponens deduction

mpiiA doubly nested modus ponens inference

syldSyllogism deduction

syldcSyllogism deduction

mp2dA double modus ponens deduction

a1ddDouble deduction introducing an antecedent

2a1ddDouble deduction introducing two antecedents

pm2.43iInference absorbing redundant antecedent

pm2.43dDeduction absorbing redundant antecedent

pm2.43aInference absorbing redundant antecedent

pm2.43bInference absorbing redundant antecedent

pm2.43Absorption of redundant antecedent

imim2dDeduction adding nested antecedents

imim2A closed form of syllogism (see syl )

embantdDeduction embedding an antecedent

3syldTriple syllogism deduction

sylsyldA double syllogism inference

imim12iInference joining two implications

imim1iInference adding common consequents in an implication, thereby interchanging the original antecedent and consequent

imim3iInference adding three nested antecedents

sylcA syllogism inference combined with contraction

syl3cA syllogism inference combined with contraction

syl6mpiA syllogism inference

mpsylModus ponens combined with a syllogism inference

mpsylsyldModus ponens combined with a double syllogism inference

syl6cInference combining syl6 with contraction

syl6ciA syllogism inference combined with contraction

sylddNested syllogism deduction

syl5dA nested syllogism deduction

syl7A syllogism rule of inference

syl6dA nested syllogism deduction

syl8A syllogism rule of inference

syl9A nested syllogism inference with different antecedents

syl9rA nested syllogism inference with different antecedents

syl10A nested syllogism inference

a1dddTriple deduction introducing an antecedent to a wff

imim12dDeduction combining antecedents and consequents

imim1dDeduction adding nested consequents

imim1A closed form of syllogism (see syl )

pm2.83Theorem *2.83 of WhiteheadRussell p. 108

peircerollOver minimal implicational calculus, Peirce's axiom peirce implies an axiom sometimes called "Roll", ( ( ph -> ps ) -> ch ) -> ( ch -> ph ) -> ph, of which looinv is a special instance

com23Commutation of antecedents

com3rCommutation of antecedents

com13Commutation of antecedents

com3lCommutation of antecedents

pm2.04Swap antecedents

com34Commutation of antecedents

com4lCommutation of antecedents

com4tCommutation of antecedents

com4rCommutation of antecedents

com24Commutation of antecedents

com14Commutation of antecedents

com45Commutation of antecedents

com35Commutation of antecedents

com25Commutation of antecedents

com5lCommutation of antecedents

com15Commutation of antecedents

com52lCommutation of antecedents

com52rCommutation of antecedents

com5rCommutation of antecedents

imim12Closed form of imim12i and of 3syl

jarrElimination of a nested antecedent

jarriInference associated with jarr

pm2.86dDeduction associated with pm2.86

pm2.86Converse of Axiom ax-2

pm2.86iInference associated with pm2.86

loolinThe Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz

loowozAn alternate for the Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz loolin, due to Barbara Wozniakowska, Reports on Mathematical Logic 10, 129-137 (1978)

Logical negation

con4Alias for ax-3 to be used instead of it for labeling consistency

con4iInference associated with con4

con4dDeduction associated with con4

mt4The rule of modus tollens

mt4dModus tollens deduction

mt4iModus tollens inference

pm2.21iA contradiction implies anything

pm2.24iiA contradiction implies anything

pm2.21dA contradiction implies anything

pm2.21ddALTAlternate proof of pm2.21dd

pm2.21From a wff and its negation, anything follows

pm2.24Theorem *2.24 of WhiteheadRussell p. 104

jarlElimination of a nested antecedent

jarliInference associated with jarl

pm2.18dDeduction form of the Clavius law pm2.18

pm2.18Clavius law, or "consequentia mirabilis" ("admirable consequence")

pm2.18iInference associated with the Clavius law pm2.18

notnotrDouble negation elimination

notnotriInference associated with notnotr

notnotriALTAlternate proof of notnotri

notnotrdDeduction associated with notnotr and notnotri

con2dA contraposition deduction

mt2dModus tollens deduction

mt2iModus tollens inference

nsyl3A negated syllogism inference

con2iA contraposition inference

nsylA negated syllogism inference

nsyl2A negated syllogism inference

notnotDouble negation introduction

notnotiInference associated with notnot

notnotdDeduction associated with notnot and notnoti

con1dA contraposition deduction

con1iA contraposition inference

mt3dModus tollens deduction

mt3iModus tollens inference

pm2.24iInference associated with pm2.24

pm2.24dDeduction form of pm2.24

con3dA contraposition deduction

con3iA contraposition inference

con3rr3Rotate through consequent right

nsyldA negated syllogism deduction

nsyliA negated syllogism inference

nsyl4A negated syllogism inference

nsyl5A negated syllogism inference

pm3.2imTheorem *3.2 of WhiteheadRussell p. 111, expressed with primitive connectives (see pm3.2 )

jcDeduction joining the consequents of two premises

jcnTheorem joining the consequents of two premises

jcndDeduction joining the consequents of two premises

impiAn importation inference

expiAn exportation inference

simprimSimplification

simplimSimplification

pm2.5gGeneral instance of Theorem *2.5 of WhiteheadRussell p. 107

pm2.5Theorem *2.5 of WhiteheadRussell p. 107

conax1Contrapositive of ax-1

conax1kWeakening of conax1

pm2.51Theorem *2.51 of WhiteheadRussell p. 107

pm2.52Theorem *2.52 of WhiteheadRussell p. 107

pm2.521gA general instance of Theorem *2.521 of WhiteheadRussell p. 107

pm2.521g2A general instance of Theorem *2.521 of WhiteheadRussell p. 107

pm2.521Theorem *2.521 of WhiteheadRussell p. 107

exptExportation theorem pm3.3 (closed form of ex) expressed with primitive connectives

exptOLDObsolete version of expt as of 25-May-2026

imptImportation theorem pm3.1 (closed form of imp) expressed with primitive connectives

pm2.61dDeduction eliminating an antecedent

pm2.61d1Inference eliminating an antecedent

pm2.61d2Inference eliminating an antecedent

pm2.61iInference eliminating an antecedent

pm2.61iiInference eliminating two antecedents

pm2.61niiInference eliminating two antecedents

pm2.61iiiInference eliminating three antecedents

jaInference joining the antecedents of two premises

jadDeduction form of ja

pm2.01Weak Clavius law

pm2.01iInference associated with the weak Clavius law pm2.01

pm2.01dDeduction based on reductio ad absurdum

pm2.6Theorem *2.6 of WhiteheadRussell p. 107

pm2.61Theorem *2.61 of WhiteheadRussell p. 107

pm2.65Theorem *2.65 of WhiteheadRussell p. 107

pm2.65iInference for proof by contradiction

pm2.65iOLDObsolete version of pm2.65i as of 7-Jun-2026

pm2.21ddA contradiction implies anything

pm2.65dDeduction for proof by contradiction

mtoThe rule of modus tollens

mtodModus tollens deduction

mtoiModus tollens inference

mt2A rule similar to modus tollens

mt3A rule similar to modus tollens

peircePeirce's axiom

looinvThe Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz

bijust0A self-implication (see id) does not imply its own negation

bijustTheorem used to justify the definition of the biconditional df-bi

Logical equivalence

impbiProperty of the biconditional connective

impbiiInfer an equivalence from an implication and its converse

impbiddDeduce an equivalence from two implications

impbid21dDeduce an equivalence from two implications

impbidDeduce an equivalence from two implications

dfbi1Relate the biconditional connective to primitive connectives

dfbi1ALTAlternate proof of dfbi1

biimpProperty of the biconditional connective

biimpiInfer an implication from a logical equivalence

sylbiA mixed syllogism inference from a biconditional and an implication

sylibA mixed syllogism inference from an implication and a biconditional

sylbbA mixed syllogism inference from two biconditionals

biimprProperty of the biconditional connective

bicom1Commutative law for the biconditional

bicomCommutative law for the biconditional

bicomdCommute two sides of a biconditional in a deduction

bicomiInference from commutative law for logical equivalence

impbid1Infer an equivalence from two implications

impbid2Infer an equivalence from two implications

impcon4bidA variation on impbid with contraposition

biimpriInfer a converse implication from a logical equivalence

biimpdDeduce an implication from a logical equivalence

mpbiAn inference from a biconditional, related to modus ponens

mpbirAn inference from a biconditional, related to modus ponens

mpbidA deduction from a biconditional, related to modus ponens

mpbiiAn inference from a nested biconditional, related to modus ponens

sylibrA mixed syllogism inference from an implication and a biconditional

sylbirA mixed syllogism inference from a biconditional and an implication

sylbbrA mixed syllogism inference from two biconditionals

sylbb1A mixed syllogism inference from two biconditionals

sylbb2A mixed syllogism inference from two biconditionals

sylibdA syllogism deduction

sylbidA syllogism deduction

mpbidiA deduction from a biconditional, related to modus ponens

biimtridA mixed syllogism inference from a nested implication and a biconditional

biimtrridA mixed syllogism inference from a nested implication and a biconditional

imbitridA mixed syllogism inference

syl5ibcomA mixed syllogism inference

imbitrridA mixed syllogism inference

syl5ibrcomA mixed syllogism inference

biimprdDeduce a converse implication from a logical equivalence

biimpcdDeduce a commuted implication from a logical equivalence

biimprcdDeduce a converse commuted implication from a logical equivalence

imbitrdiA mixed syllogism inference from a nested implication and a biconditional

imbitrrdiA mixed syllogism inference from a nested implication and a biconditional

biimtrdiA mixed syllogism inference

biimtrrdiA mixed syllogism inference

syl7biA mixed syllogism inference from a doubly nested implication and a biconditional

syl8ibA syllogism rule of inference

mpbirdA deduction from a biconditional, related to modus ponens

mpbiriAn inference from a nested biconditional, related to modus ponens

sylibrdA syllogism deduction

sylbirdA syllogism deduction

biidPrinciple of identity for logical equivalence

biiddPrinciple of identity with antecedent

pm5.1imTwo propositions are equivalent if they are both true

2thTwo truths are equivalent

2thdTwo truths are equivalent

monotheticTwo self-implications (see id) are equivalent

ibiInference that converts a biconditional implied by one of its arguments, into an implication

ibirInference that converts a biconditional implied by one of its arguments, into an implication

ibdDeduction that converts a biconditional implied by one of its arguments, into an implication

pm5.74Distribution of implication over biconditional

pm5.74iDistribution of implication over biconditional (inference form)

pm5.74riDistribution of implication over biconditional (reverse inference form)

pm5.74dDistribution of implication over biconditional (deduction form)

pm5.74rdDistribution of implication over biconditional (deduction form)

bitriAn inference from transitive law for logical equivalence

bitr2iAn inference from transitive law for logical equivalence

bitr3iAn inference from transitive law for logical equivalence

bitr4iAn inference from transitive law for logical equivalence

bitrdDeduction form of bitri

bitr2dDeduction form of bitr2i

bitr3dDeduction form of bitr3i

bitr4dDeduction form of bitr4i

bitridA syllogism inference from two biconditionals

bitr2idA syllogism inference from two biconditionals

bitr3idA syllogism inference from two biconditionals

bitr3diA syllogism inference from two biconditionals

bitrdiA syllogism inference from two biconditionals

bitr2diA syllogism inference from two biconditionals

bitr4diA syllogism inference from two biconditionals

bitr4idA syllogism inference from two biconditionals

3imtr3iA mixed syllogism inference, useful for removing a definition from both sides of an implication

3imtr4iA mixed syllogism inference, useful for applying a definition to both sides of an implication

3imtr3dMore general version of 3imtr3i

3imtr4dMore general version of 3imtr4i

3imtr3gMore general version of 3imtr3i

3imtr4gMore general version of 3imtr4i

3bitriA chained inference from transitive law for logical equivalence

3bitrriA chained inference from transitive law for logical equivalence

3bitr2iA chained inference from transitive law for logical equivalence

3bitr2riA chained inference from transitive law for logical equivalence

3bitr3iA chained inference from transitive law for logical equivalence

3bitr3riA chained inference from transitive law for logical equivalence

3bitr4iA chained inference from transitive law for logical equivalence

3bitr4riA chained inference from transitive law for logical equivalence

3bitrdDeduction from transitivity of biconditional

3bitrrdDeduction from transitivity of biconditional

3bitr2dDeduction from transitivity of biconditional

3bitr2rdDeduction from transitivity of biconditional

3bitr3dDeduction from transitivity of biconditional

3bitr3rdDeduction from transitivity of biconditional

3bitr4dDeduction from transitivity of biconditional

3bitr4rdDeduction from transitivity of biconditional

3bitr3gMore general version of 3bitr3i

3bitr4gMore general version of 3bitr4i

notnotbDouble negation

con34bA biconditional form of contraposition

con4bidA contraposition deduction

notbidDeduction negating both sides of a logical equivalence

notbiiNegate both sides of a logical equivalence

con4biiA contraposition inference

mtbiAn inference from a biconditional, related to modus tollens

mtbirAn inference from a biconditional, related to modus tollens

mtbidA deduction from a biconditional, similar to modus tollens

mtbirdA deduction from a biconditional, similar to modus tollens

mtbiiAn inference from a biconditional, similar to modus tollens

mtbiriAn inference from a biconditional, similar to modus tollens

sylnibA mixed syllogism inference from an implication and a biconditional

sylnibrA mixed syllogism inference from an implication and a biconditional

sylnbiA mixed syllogism inference from a biconditional and an implication

sylnbirA mixed syllogism inference from a biconditional and an implication

xchnxbiReplacement of a subexpression by an equivalent one

xchnxbirReplacement of a subexpression by an equivalent one

xchbinxReplacement of a subexpression by an equivalent one

xchbinxrReplacement of a subexpression by an equivalent one

imbi2iIntroduce an antecedent to both sides of a logical equivalence

bibi2iInference adding a biconditional to the left in an equivalence

bibi1iInference adding a biconditional to the right in an equivalence

bibi12iThe equivalence of two equivalences

imbi2dDeduction adding an antecedent to both sides of a logical equivalence

imbi1dDeduction adding a consequent to both sides of a logical equivalence

bibi2dDeduction adding a biconditional to the left in an equivalence

bibi1dDeduction adding a biconditional to the right in an equivalence

imbi12dDeduction joining two equivalences to form equivalence of implications

bibi12dDeduction joining two equivalences to form equivalence of biconditionals

imbi12Closed form of imbi12i

imbi1Theorem *4.84 of WhiteheadRussell p. 122

imbi2Theorem *4.85 of WhiteheadRussell p. 122

imbi1iIntroduce a consequent to both sides of a logical equivalence

imbi12iJoin two logical equivalences to form equivalence of implications

bibi1Theorem *4.86 of WhiteheadRussell p. 122

bitr3Closed nested implication form of bitr3i

con2biContraposition

con2bidA contraposition deduction

con1bidA contraposition deduction

con1biiA contraposition inference

con2biiA contraposition inference

biimtA wff is equivalent to itself with true antecedent

pm5.5Theorem *5.5 of WhiteheadRussell p. 125

a1biInference introducing a theorem as an antecedent

mt2biA false consequent falsifies an antecedent

mttModus-tollens-like theorem

imnotIf a proposition is false, then implying it is equivalent to being false

pm5.501Theorem *5.501 of WhiteheadRussell p. 125

ibibImplication in terms of implication and biconditional

ibibrImplication in terms of implication and biconditional

tbtA wff is equivalent to its equivalence with a truth

nbn2The negation of a wff is equivalent to the wff's equivalence to falsehood

bibifTransfer negation via an equivalence

nbnThe negation of a wff is equivalent to the wff's equivalence to falsehood

nbn3Transfer falsehood via equivalence

pm5.21imTwo propositions are equivalent if they are both false

2falseTwo falsehoods are equivalent

2falsedTwo falsehoods are equivalent (deduction form)

pm5.21niTwo propositions implying a false one are equivalent

pm5.21niiEliminate an antecedent implied by each side of a biconditional

pm5.21nddEliminate an antecedent implied by each side of a biconditional, deduction version

bijaCombine antecedents into a single biconditional

pm5.18Theorem *5.18 of WhiteheadRussell p. 124

xor3Two ways to express "exclusive or"

nbbnMove negation outside of biconditional

nbbnOLDObsolete version of nbbn as of 10-Jun-2026

biassAssociative law for the biconditional

birotRotation of the arguments of the nested implication (

bilukLukasiewicz's shortest axiom for equivalential calculus

pm5.19Theorem *5.19 of WhiteheadRussell p. 124

bi2.04Logical equivalence of commuted antecedents

pm5.4Antecedent absorption implication

imdiDistributive law for implication

pm5.41Theorem *5.41 of WhiteheadRussell p. 125

imbibiThe antecedent of one side of a biconditional can be moved out of the biconditional to become the antecedent of the remaining biconditional

imbibiOLDObsolete version of imbibi as of 15-Jun-2026

pm4.8Theorem *4.8 of WhiteheadRussell p. 122

pm4.81A formula is equivalent to its negation implying it

imim21bSimplify an implication between two implications when the antecedent of the first is a consequence of the antecedent of the second

Logical conjunction

pm4.63Theorem *4.63 of WhiteheadRussell p. 120

pm4.67Theorem *4.67 of WhiteheadRussell p. 120

imnanExpress an implication in terms of a negated conjunction

imnaniInfer an implication from a negated conjunction

imanImplication in terms of conjunction and negation

pm3.24Law of noncontradiction

annimExpress a conjunction in terms of a negated implication

pm4.61Theorem *4.61 of WhiteheadRussell p. 120

pm4.65Theorem *4.65 of WhiteheadRussell p. 120

impImportation inference

impcomImportation inference with commuted antecedents

con3dimpVariant of con3d with importation

mpnanrdEliminate the right side of a negated conjunction in an implication

impdImportation deduction

impcomdImportation deduction with commuted antecedents

exExportation inference

expcomExportation inference with commuted antecedents

expdcomCommuted form of expd

expdExportation deduction

expcomdDeduction form of expcom

imp31An importation inference

imp32An importation inference

exp31An exportation inference

exp32An exportation inference

imp4bAn importation inference

imp4aAn importation inference

imp4cAn importation inference

imp4dAn importation inference

imp41An importation inference

imp42An importation inference

imp43An importation inference

imp44An importation inference

imp45An importation inference

exp4bAn exportation inference

exp4aAn exportation inference

exp4cAn exportation inference

exp4dAn exportation inference

exp41An exportation inference

exp42An exportation inference

exp43An exportation inference

exp44An exportation inference

exp45An exportation inference

imp5dAn importation inference

imp5aAn importation inference

imp5gAn importation inference

imp55An importation inference

imp511An importation inference

exp5cAn exportation inference

exp5jAn exportation inference

exp5lAn exportation inference

exp53An exportation inference

pm3.3Theorem *3.3 (Exp) of WhiteheadRussell p. 112

pm3.31Theorem *3.31 (Imp) of WhiteheadRussell p. 112

impexpImport-export theorem

impancomMixed importation/commutation inference

expdimpA deduction version of exportation, followed by importation

expimpdExportation followed by a deduction version of importation

imprImport a wff into a right conjunct

implExport a wff from a left conjunct

exprExport a wff from a right conjunct

explExport a wff from a left conjunct

ancomsInference commuting conjunction in antecedent

pm3.22Theorem *3.22 of WhiteheadRussell p. 111

ancomCommutative law for conjunction

ancomdCommutation of conjuncts in consequent

biancomiCommuting conjunction in a biconditional

biancomdCommuting conjunction in a biconditional, deduction form

ancomstClosed form of ancoms

ancomsdDeduction commuting conjunction in antecedent

anasssAssociative law for conjunction applied to antecedent (eliminates syllogism)

anassrsAssociative law for conjunction applied to antecedent (eliminates syllogism)

anassAssociative law for conjunction

pm3.2Join antecedents with conjunction ("conjunction introduction")

pm3.2iInfer conjunction of premises

pm3.21Join antecedents with conjunction

pm3.43iNested conjunction of antecedents

pm3.43Theorem *3.43 (Comp) of WhiteheadRussell p. 113

dfbi2A theorem similar to the standard definition of the biconditional

dfbiDefinition df-bi rewritten in an abbreviated form to help intuitive understanding of that definition

biimpaImportation inference from a logical equivalence

biimparImportation inference from a logical equivalence

biimpacImportation inference from a logical equivalence

biimparcImportation inference from a logical equivalence

adantrInference adding a conjunct to the right of an antecedent

adantlInference adding a conjunct to the left of an antecedent

simplElimination of a conjunct

simpliInference eliminating a conjunct

simprElimination of a conjunct

simpriInference eliminating a conjunct

intnanIntroduction of conjunct inside of a contradiction

intnanrIntroduction of conjunct inside of a contradiction

intnandIntroduction of conjunct inside of a contradiction

intnanrdIntroduction of conjunct inside of a contradiction

adantldDeduction adding a conjunct to the left of an antecedent

adantrdDeduction adding a conjunct to the right of an antecedent

pm3.41Theorem *3.41 of WhiteheadRussell p. 113

pm3.42Theorem *3.42 of WhiteheadRussell p. 113

simpldDeduction eliminating a conjunct

simprdDeduction eliminating a conjunct

simplbiDeduction eliminating a conjunct

simprbiDeduction eliminating a conjunct

simprbdaDeduction eliminating a conjunct

simplbdaDeduction eliminating a conjunct

simplbi2Deduction eliminating a conjunct

simplbi2comtClosed form of simplbi2com

simplbi2comA deduction eliminating a conjunct, similar to simplbi2

biraniInference adding a conjunct to the left-hand side of a biconditional

bilaniInference adding a conjunct to the left-hand side of a biconditional

biranriInference adding a conjunct to the right-hand side of a biconditional

bilanriInference adding a conjunct to the right-hand side of a biconditional

simpl2imImplication from an eliminated conjunct implied by the antecedent

simplbiimImplication from an eliminated conjunct equivalent to the antecedent

impelAn inference for implication elimination

mpan9Modus ponens conjoining dissimilar antecedents

sylan9Nested syllogism inference conjoining dissimilar antecedents

sylan9rNested syllogism inference conjoining dissimilar antecedents

sylan9bbNested syllogism inference conjoining dissimilar antecedents

sylan9bbrNested syllogism inference conjoining dissimilar antecedents

jcaDeduce conjunction of the consequents of two implications ("join consequents with 'and'")

jcadDeduction conjoining the consequents of two implications

jca2Inference conjoining the consequents of two implications

jca31Join three consequents

jca32Join three consequents

jcaiDeduction replacing implication with conjunction

jcabDistributive law for implication over conjunction

pm4.76Theorem *4.76 of WhiteheadRussell p. 121

jctilInference conjoining a theorem to left of consequent in an implication

jctirInference conjoining a theorem to right of consequent in an implication

jccirInference conjoining a consequent of a consequent to the right of the consequent in an implication

jccilInference conjoining a consequent of a consequent to the left of the consequent in an implication

jctlInference conjoining a theorem to the left of a consequent

jctrInference conjoining a theorem to the right of a consequent

jctildDeduction conjoining a theorem to left of consequent in an implication

jctirdDeduction conjoining a theorem to right of consequent in an implication

ibaIntroduction of antecedent as conjunct

ibarIntroduction of antecedent as conjunct

biantruA wff is equivalent to its conjunction with truth

biantrurA wff is equivalent to its conjunction with truth

biantrudA wff is equivalent to its conjunction with truth

biantrurdA wff is equivalent to its conjunction with truth

bianfiA wff conjoined with falsehood is false

bianfdA wff conjoined with falsehood is false

baibMove conjunction outside of biconditional

baibrMove conjunction outside of biconditional

rbaibrMove conjunction outside of biconditional

rbaibMove conjunction outside of biconditional

baibdMove conjunction outside of biconditional

rbaibdMove conjunction outside of biconditional

bianabsAbsorb a hypothesis into the second member of a biconditional

pm5.44Theorem *5.44 of WhiteheadRussell p. 125

pm5.42Theorem *5.42 of WhiteheadRussell p. 125

anclConjoin antecedent to left of consequent

anclbConjoin antecedent to left of consequent

ancrConjoin antecedent to right of consequent

ancrbConjoin antecedent to right of consequent

ancliDeduction conjoining antecedent to left of consequent

ancriDeduction conjoining antecedent to right of consequent

ancldDeduction conjoining antecedent to left of consequent in nested implication

ancrdDeduction conjoining antecedent to right of consequent in nested implication

impacImportation with conjunction in consequent

anc2lConjoin antecedent to left of consequent in nested implication

anc2rConjoin antecedent to right of consequent in nested implication

anc2liDeduction conjoining antecedent to left of consequent in nested implication

anc2riDeduction conjoining antecedent to right of consequent in nested implication

pm4.71Implication in terms of biconditional and conjunction

pm4.71rImplication in terms of biconditional and conjunction

pm4.71iInference converting an implication to a biconditional with conjunction

pm4.71riInference converting an implication to a biconditional with conjunction

pm4.71dDeduction converting an implication to a biconditional with conjunction

pm4.71rdDeduction converting an implication to a biconditional with conjunction

pm4.71daDeduction converting a biconditional to a biconditional with conjunction

pm4.24Theorem *4.24 of WhiteheadRussell p. 117

anidmIdempotent law for conjunction

anidmdbiConjunction idempotence with antecedent

anidmsInference from idempotent law for conjunction

imdistanDistribution of implication with conjunction

imdistaniDistribution of implication with conjunction

imdistanriDistribution of implication with conjunction

imdistandDistribution of implication with conjunction (deduction form)

imdistandaDistribution of implication with conjunction (deduction version with conjoined antecedent)

pm5.3Theorem *5.3 of WhiteheadRussell p. 125

pm5.32Distribution of implication over biconditional

pm5.32iDistribution of implication over biconditional (inference form)

pm5.32riDistribution of implication over biconditional (inference form)

bianimExchanging conjunction in a biconditional

pm5.32dDistribution of implication over biconditional (deduction form)

pm5.32rdDistribution of implication over biconditional (deduction form)

pm5.32daDistribution of implication over biconditional (deduction form)

bian1dAdding a superfluous conjunct in a biconditional

sylanA syllogism inference

sylanbA syllogism inference

sylanbrA syllogism inference

sylanbrcSyllogism inference

syl2ancSyllogism inference combined with contraction

syl2anc2Double syllogism inference combined with contraction

sylanclSyllogism inference combined with modus ponens

sylancrSyllogism inference combined with modus ponens

sylancomSyllogism inference with commutation of antecedents

sylanblcSyllogism inference combined with a biconditional

sylanblrcSyllogism inference combined with a biconditional

syldanA syllogism deduction with conjoined antecedents

sylbidaA syllogism deduction

sylan2A syllogism inference

sylan2bA syllogism inference

sylan2brA syllogism inference

syl2anA double syllogism inference

syl2anrA double syllogism inference

syl2anbA double syllogism inference

syl2anbrA double syllogism inference

sylancbA syllogism inference combined with contraction

sylancbrA syllogism inference combined with contraction

syldanlA syllogism deduction with conjoined antecedents

sylandA syllogism deduction

sylaniA syllogism inference

sylan2dA syllogism deduction

sylan2iA syllogism inference

syl2aniA syllogism inference

syl2andA syllogism deduction

anim12dConjoin antecedents and consequents in a deduction

anim12d1Variant of anim12d where the second implication does not depend on the antecedent

anim1dAdd a conjunct to right of antecedent and consequent in a deduction

anim2dAdd a conjunct to left of antecedent and consequent in a deduction

anim12iConjoin antecedents and consequents of two premises

anim12ciVariant of anim12i with commutation

anim1iIntroduce conjunct to both sides of an implication

anim1ciIntroduce conjunct to both sides of an implication

anim2iIntroduce conjunct to both sides of an implication

anim12iiConjoin antecedents and consequents in a deduction

anim12danConjoin antecedents and consequents in a deduction

im2anan9Deduction joining nested implications to form implication of conjunctions

im2anan9rDeduction joining nested implications to form implication of conjunctions

pm3.45Theorem *3.45 (Fact) of WhiteheadRussell p. 113

anbi2iIntroduce a left conjunct to both sides of a logical equivalence

anbi1iIntroduce a right conjunct to both sides of a logical equivalence

anbi2ciVariant of anbi2i with commutation

anbi1ciVariant of anbi1i with commutation

bianbiExchanging conjunction in a biconditional

anbi12iConjoin both sides of two equivalences

anbi12ciVariant of anbi12i with commutation

anbi2dDeduction adding a left conjunct to both sides of a logical equivalence

anbi1dDeduction adding a right conjunct to both sides of a logical equivalence

anbi12dDeduction joining two equivalences to form equivalence of conjunctions

anbi1Introduce a right conjunct to both sides of a logical equivalence

anbi2Introduce a left conjunct to both sides of a logical equivalence

anbi1cdIntroduce a proposition as left conjunct on the left-hand side and right conjunct on the right-hand side of an equivalence

an2anrDouble commutation in conjunction

pm4.38Theorem *4.38 of WhiteheadRussell p. 118

bi2anan9Deduction joining two equivalences to form equivalence of conjunctions

bi2anan9rDeduction joining two equivalences to form equivalence of conjunctions

bi2bian9Deduction joining two biconditionals with different antecedents

anbiimAdding biconditional when antecedents are conjuncted

anbiimOLDObsolete version of anbiim as of 15-Jun-2026

bianassAn inference to merge two lists of conjuncts

bianasscAn inference to merge two lists of conjuncts

an21Swap two conjuncts

an12Swap two conjuncts

an32A rearrangement of conjuncts

an13A rearrangement of conjuncts

an31A rearrangement of conjuncts

an12sSwap two conjuncts in antecedent

ancom2sInference commuting a nested conjunction in antecedent

an13sSwap two conjuncts in antecedent

an32sSwap two conjuncts in antecedent

ancom1sInference commuting a nested conjunction in antecedent

an31sSwap two conjuncts in antecedent

anass1rsCommutative-associative law for conjunction in an antecedent

an4Rearrangement of 4 conjuncts

an42Rearrangement of 4 conjuncts

an43Rearrangement of 4 conjuncts

an3A rearrangement of conjuncts

an4sInference rearranging 4 conjuncts in antecedent

an42sInference rearranging 4 conjuncts in antecedent

anabs1Absorption into embedded conjunct

anabs5Absorption into embedded conjunct

anabs7Absorption into embedded conjunct

anabsanAbsorption of antecedent with conjunction

anabss1Absorption of antecedent into conjunction

anabss4Absorption of antecedent into conjunction

anabss5Absorption of antecedent into conjunction

anabsi5Absorption of antecedent into conjunction

anabsi6Absorption of antecedent into conjunction

anabsi7Absorption of antecedent into conjunction

anabsi8Absorption of antecedent into conjunction

anabss7Absorption of antecedent into conjunction

anabsan2Absorption of antecedent with conjunction

anabss3Absorption of antecedent into conjunction

anandiDistribution of conjunction over conjunction

anandirDistribution of conjunction over conjunction

anandisInference that undistributes conjunction in the antecedent

anandirsInference that undistributes conjunction in the antecedent

sylanl1A syllogism inference

sylanl2A syllogism inference

sylanr1A syllogism inference

sylanr2A syllogism inference

syl6anA syllogism deduction combined with conjoining antecedents

syl2an2rsyl2anr with antecedents in standard conjunction form

syl2an2syl2an with antecedents in standard conjunction form

mpdanAn inference based on modus ponens

mpancomAn inference based on modus ponens with commutation of antecedents

mpidanA deduction which "stacks" a hypothesis

mpanAn inference based on modus ponens

mpan2An inference based on modus ponens

mp2anAn inference based on modus ponens

mp4anAn inference based on modus ponens

mpan2dA deduction based on modus ponens

mpandA deduction based on modus ponens

mpaniAn inference based on modus ponens

mpan2iAn inference based on modus ponens

mp2aniAn inference based on modus ponens

mp2andA deduction based on modus ponens

mpanl1An inference based on modus ponens

mpanl2An inference based on modus ponens

mpanl12An inference based on modus ponens

mpanr1An inference based on modus ponens

mpanr2An inference based on modus ponens

mpanr12An inference based on modus ponens

mpanlr1An inference based on modus ponens

mpbirandDetach truth from conjunction in biconditional

mpbiran2dDetach truth from conjunction in biconditional

mpbiranDetach truth from conjunction in biconditional

mpbiran2Detach truth from conjunction in biconditional

mpbir2anDetach a conjunction of truths in a biconditional

mpbi2andDetach a conjunction of truths in a biconditional

mpbir2andDetach a conjunction of truths in a biconditional

adantllDeduction adding a conjunct to antecedent

adantlrDeduction adding a conjunct to antecedent

adantrlDeduction adding a conjunct to antecedent

adantrrDeduction adding a conjunct to antecedent

adantlllDeduction adding a conjunct to antecedent

adantllrDeduction adding a conjunct to antecedent

adantlrlDeduction adding a conjunct to antecedent

adantlrrDeduction adding a conjunct to antecedent

adantrllDeduction adding a conjunct to antecedent

adantrlrDeduction adding a conjunct to antecedent

adantrrlDeduction adding a conjunct to antecedent

adantrrrDeduction adding a conjunct to antecedent

ad2antrrDeduction adding two conjuncts to antecedent

ad2antlrDeduction adding two conjuncts to antecedent

ad2antrlDeduction adding two conjuncts to antecedent

ad2antllDeduction adding conjuncts to antecedent

ad3antrrrDeduction adding three conjuncts to antecedent

ad3antlrDeduction adding three conjuncts to antecedent

ad4antrDeduction adding 4 conjuncts to antecedent

ad4antlrDeduction adding 4 conjuncts to antecedent

ad5antrDeduction adding 5 conjuncts to antecedent

ad5antlrDeduction adding 5 conjuncts to antecedent

ad6antrDeduction adding 6 conjuncts to antecedent

ad6antlrDeduction adding 6 conjuncts to antecedent

ad7antrDeduction adding 7 conjuncts to antecedent

ad7antlrDeduction adding 7 conjuncts to antecedent

ad8antrDeduction adding 8 conjuncts to antecedent

ad8antlrDeduction adding 8 conjuncts to antecedent

ad9antrDeduction adding 9 conjuncts to antecedent

ad9antlrDeduction adding 9 conjuncts to antecedent

ad10antrDeduction adding 10 conjuncts to antecedent

ad10antlrDeduction adding 10 conjuncts to antecedent

ad2ant2lDeduction adding two conjuncts to antecedent

ad2ant2rDeduction adding two conjuncts to antecedent

ad2ant2lrDeduction adding two conjuncts to antecedent

ad2ant2rlDeduction adding two conjuncts to antecedent

adantl3rDeduction adding 1 conjunct to antecedent

ad4ant13Deduction adding conjuncts to antecedent

ad4ant14Deduction adding conjuncts to antecedent

ad4ant23Deduction adding conjuncts to antecedent

ad4ant24Deduction adding conjuncts to antecedent

adantl4rDeduction adding 1 conjunct to antecedent

ad5ant13Deduction adding conjuncts to antecedent

ad5ant14Deduction adding conjuncts to antecedent

ad5ant15Deduction adding conjuncts to antecedent

ad5ant23Deduction adding conjuncts to antecedent

ad5ant24Deduction adding conjuncts to antecedent

ad5ant25Deduction adding conjuncts to antecedent

adantl5rDeduction adding 1 conjunct to antecedent

adantl6rDeduction adding 1 conjunct to antecedent

pm3.33Theorem *3.33 (Syll) of WhiteheadRussell p. 112

pm3.34Theorem *3.34 (Syll) of WhiteheadRussell p. 112

simpllSimplification of a conjunction

simplldDeduction form of simpll, eliminating a double conjunct

simplrSimplification of a conjunction

simplrdDeduction eliminating a double conjunct

simprlSimplification of a conjunction

simprldDeduction eliminating a double conjunct

simprrSimplification of a conjunction

simprrdDeduction form of simprr, eliminating a double conjunct

simplllSimplification of a conjunction

simpllrSimplification of a conjunction

simplrlSimplification of a conjunction

simplrrSimplification of a conjunction

simprllSimplification of a conjunction

simprlrSimplification of a conjunction

simprrlSimplification of a conjunction

simprrrSimplification of a conjunction

simp-4lSimplification of a conjunction

simp-4rSimplification of a conjunction

simp-5lSimplification of a conjunction

simp-5rSimplification of a conjunction

simp-6lSimplification of a conjunction

simp-6rSimplification of a conjunction

simp-7lSimplification of a conjunction

simp-7rSimplification of a conjunction

simp-8lSimplification of a conjunction

simp-8rSimplification of a conjunction

simp-9lSimplification of a conjunction

simp-9rSimplification of a conjunction

simp-10lSimplification of a conjunction

simp-10rSimplification of a conjunction

simp-11lSimplification of a conjunction

simp-11rSimplification of a conjunction

pm2.01daDeduction based on reductio ad absurdum

pm2.18daDeduction based on reductio ad absurdum

impbidaDeduce an equivalence from two implications

pm5.21ndEliminate an antecedent implied by each side of a biconditional

pm3.35Conjunctive detachment

pm5.74daDistribution of implication over biconditional (deduction form)

bitrTheorem *4.22 of WhiteheadRussell p. 117

biantrA transitive law of equivalence

pm4.14Theorem *4.14 of WhiteheadRussell p. 117

pm3.37Theorem *3.37 (Transp) of WhiteheadRussell p. 112

anim12Conjoin antecedents and consequents of two premises

pm3.4Conjunction implies implication

exbiriInference form of exbir

pm2.61ianElimination of an antecedent

pm2.61danElimination of an antecedent

pm2.61ddanElimination of two antecedents

pm2.61ddaElimination of two antecedents

mtandA modus tollens deduction

pm2.65daDeduction for proof by contradiction

condanProof by contradiction

biadanAn implication is equivalent to the equivalence of some implied equivalence and some other equivalence involving a conjunction

biadaniInference associated with biadan

biadaniALTAlternate proof of biadani not using biadan

biadaniiInference associated with biadani

biadanidDeduction associated with biadani

pm5.1Two propositions are equivalent if they are both true

pm5.21Two propositions are equivalent if they are both false

pm5.35Theorem *5.35 of WhiteheadRussell p. 125

abaiIntroduce one conjunct as an antecedent to the other

ababIntroduce one conjunct as equivalent to the other

pm4.45imConjunction with implication

impimprbiAn implication and its reverse are equivalent exactly when both operands are equivalent

nanTheorem to move a conjunct in and out of a negation

pm5.31Theorem *5.31 of WhiteheadRussell p. 125

pm5.31rVariant of pm5.31

pm4.15Theorem *4.15 of WhiteheadRussell p. 117

pm5.36Theorem *5.36 of WhiteheadRussell p. 125

annotanannotA conjunction with a negated conjunction

pm5.33Theorem *5.33 of WhiteheadRussell p. 125

syl12ancSyllogism combined with contraction

syl21ancSyllogism combined with contraction

syl22ancSyllogism combined with contraction

bibiadEliminate an hypothesis th in a biconditional

syl1111ancFour-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection

syldbl2Stacked hypotheseis implies goal

mpsyl4ancAn elimination deduction

pm4.87Theorem *4.87 of WhiteheadRussell p. 122

bimsc1Removal of conjunct from one side of an equivalence

a2andDeduction distributing a conjunction as embedded antecedent

animpimp2impdDeduction deriving nested implications from conjunctions

Logical disjunction

pm4.64Theorem *4.64 of WhiteheadRussell p. 120

pm4.66Theorem *4.66 of WhiteheadRussell p. 120

pm2.53Theorem *2.53 of WhiteheadRussell p. 107

pm2.54Theorem *2.54 of WhiteheadRussell p. 107

imorImplication in terms of disjunction

imoriInfer disjunction from implication

imorriInfer implication from disjunction

pm4.62Theorem *4.62 of WhiteheadRussell p. 120

jaoiInference disjoining the antecedents of two implications

jao1iAdd a disjunct in the antecedent of an implication

jaodDeduction disjoining the antecedents of two implications

mpjaodEliminate a disjunction in a deduction

oriInfer implication from disjunction

orriInfer disjunction from implication

orrdDeduce disjunction from implication

ordDeduce implication from disjunction

orciDeduction introducing a disjunct

olciDeduction introducing a disjunct

orcIntroduction of a disjunct

olcIntroduction of a disjunct

pm1.4Axiom *1.4 of WhiteheadRussell p. 96

orcomCommutative law for disjunction

orcomdCommutation of disjuncts in consequent

orcomsCommutation of disjuncts in antecedent

orcdDeduction introducing a disjunct

olcdDeduction introducing a disjunct

orcsDeduction eliminating disjunct

olcsDeduction eliminating disjunct

olcndA lemma for Conjunctive Normal Form unit propagation, in deduction form

orcndA lemma for Conjunctive Normal Form unit propagation, in deduction form

mtordA modus tollens deduction involving disjunction

pm3.2niInfer negated disjunction of negated premises

pm2.45Theorem *2.45 of WhiteheadRussell p. 106

pm2.46Theorem *2.46 of WhiteheadRussell p. 106

pm2.47Theorem *2.47 of WhiteheadRussell p. 107

pm2.48Theorem *2.48 of WhiteheadRussell p. 107

pm2.49Theorem *2.49 of WhiteheadRussell p. 107

norbiIf neither of two propositions is true, then these propositions are equivalent

nbiorIf two propositions are not equivalent, then at least one is true

orel1Elimination of disjunction by denial of a disjunct

pm2.25Theorem *2.25 of WhiteheadRussell p. 104

orel2Elimination of disjunction by denial of a disjunct

pm2.67-2Slight generalization of Theorem *2.67 of WhiteheadRussell p. 107

pm2.67Theorem *2.67 of WhiteheadRussell p. 107

curryaxA non-intuitionistic positive statement, sometimes called a paradox of material implication

exmidLaw of excluded middle, also called the principle of tertium non datur

exmiddLaw of excluded middle in a context

pm2.1Theorem *2.1 of WhiteheadRussell p. 101

pm2.13Theorem *2.13 of WhiteheadRussell p. 101

pm2.621Theorem *2.621 of WhiteheadRussell p. 107

pm2.62Theorem *2.62 of WhiteheadRussell p. 107

pm2.68Theorem *2.68 of WhiteheadRussell p. 108

dfor2Logical 'or' expressed in terms of implication only

pm2.07Theorem *2.07 of WhiteheadRussell p. 101

pm1.2Axiom *1.2 of WhiteheadRussell p. 96, which they call "Taut"

oridmIdempotent law for disjunction

pm4.25Theorem *4.25 of WhiteheadRussell p. 117

pm2.4Theorem *2.4 of WhiteheadRussell p. 106

pm2.41Theorem *2.41 of WhiteheadRussell p. 106

orim12iDisjoin antecedents and consequents of two premises

orim1iIntroduce disjunct to both sides of an implication

orim2iIntroduce disjunct to both sides of an implication

orim12dALTAlternate proof of orim12d which does not depend on df-an

orbi2iInference adding a left disjunct to both sides of a logical equivalence

orbi1iInference adding a right disjunct to both sides of a logical equivalence

orbi12iInfer the disjunction of two equivalences

orbi2dDeduction adding a left disjunct to both sides of a logical equivalence

orbi1dDeduction adding a right disjunct to both sides of a logical equivalence

orbi1Theorem *4.37 of WhiteheadRussell p. 118

orbi12dDeduction joining two equivalences to form equivalence of disjunctions

pm1.5Axiom *1.5 (Assoc) of WhiteheadRussell p. 96

or12Swap two disjuncts

orassAssociative law for disjunction

pm2.31Theorem *2.31 of WhiteheadRussell p. 104

pm2.32Theorem *2.32 of WhiteheadRussell p. 105

pm2.3Theorem *2.3 of WhiteheadRussell p. 104

or32A rearrangement of disjuncts

or4Rearrangement of 4 disjuncts

or42Rearrangement of 4 disjuncts

orordiDistribution of disjunction over disjunction

orordirDistribution of disjunction over disjunction

orimdiDisjunction distributes over implication

pm2.76Theorem *2.76 of WhiteheadRussell p. 108

pm2.85Theorem *2.85 of WhiteheadRussell p. 108

pm2.75Theorem *2.75 of WhiteheadRussell p. 108

pm4.78Implication distributes over disjunction

biortA disjunction with a true formula is equivalent to that true formula

biorfA wff is equivalent to its disjunction with falsehood

biortnA wff is equivalent to its negated disjunction with falsehood

biorfiThe dual of biorf is not biantr but iba (and ibar )

biorfriA wff is equivalent to its disjunction with falsehood

pm2.26Theorem *2.26 of WhiteheadRussell p. 104

pm2.63Theorem *2.63 of WhiteheadRussell p. 107

pm2.64Theorem *2.64 of WhiteheadRussell p. 107

pm2.42Theorem *2.42 of WhiteheadRussell p. 106

pm5.11gA general instance of Theorem *5.11 of WhiteheadRussell p. 123

pm5.11Theorem *5.11 of WhiteheadRussell p. 123

pm5.12Theorem *5.12 of WhiteheadRussell p. 123

pm5.14Theorem *5.14 of WhiteheadRussell p. 123

pm5.13Theorem *5.13 of WhiteheadRussell p. 123

pm5.55Theorem *5.55 of WhiteheadRussell p. 125

pm4.72Implication in terms of biconditional and disjunction

imimorbSimplify an implication between implications

oibabsAbsorption of disjunction into equivalence

orbidiDisjunction distributes over the biconditional

pm5.7Disjunction distributes over the biconditional

Mixed connectives

jaaoInference conjoining and disjoining the antecedents of two implications

jaoaInference disjoining and conjoining the antecedents of two implications

jaoianInference disjoining the antecedents of two implications

jaodanDeduction disjoining the antecedents of two implications

mpjaodanEliminate a disjunction in a deduction

pm3.44Theorem *3.44 of WhiteheadRussell p. 113

jaoDisjunction of antecedents

jaobDisjunction of antecedents

pm4.77Theorem *4.77 of WhiteheadRussell p. 121

pm3.48Theorem *3.48 of WhiteheadRussell p. 114

orim12dDisjoin antecedents and consequents in a deduction

orim12daDeduce a disjunction from another one

orim1dDisjoin antecedents and consequents in a deduction

orim2dDisjoin antecedents and consequents in a deduction

orim2Axiom *1.6 (Sum) of WhiteheadRussell p. 97

pm2.38Theorem *2.38 of WhiteheadRussell p. 105

pm2.36Theorem *2.36 of WhiteheadRussell p. 105

pm2.37Theorem *2.37 of WhiteheadRussell p. 105

pm2.81Theorem *2.81 of WhiteheadRussell p. 108

pm2.8Theorem *2.8 of WhiteheadRussell p. 108

pm2.73Theorem *2.73 of WhiteheadRussell p. 108

pm2.74Theorem *2.74 of WhiteheadRussell p. 108

pm2.82Theorem *2.82 of WhiteheadRussell p. 108

pm4.39Theorem *4.39 of WhiteheadRussell p. 118

animorlConjunction implies disjunction with one common formula (1/4)

animorrConjunction implies disjunction with one common formula (2/4)

animorlrConjunction implies disjunction with one common formula (3/4)

animorrlConjunction implies disjunction with one common formula (4/4)

ianorNegated conjunction in terms of disjunction (De Morgan's law)

anorConjunction in terms of disjunction (De Morgan's law)

ioranNegated disjunction in terms of conjunction (De Morgan's law)

pm4.52Theorem *4.52 of WhiteheadRussell p. 120

pm4.53Theorem *4.53 of WhiteheadRussell p. 120

pm4.54Theorem *4.54 of WhiteheadRussell p. 120

pm4.55Theorem *4.55 of WhiteheadRussell p. 120

pm4.56Theorem *4.56 of WhiteheadRussell p. 120

oranDisjunction in terms of conjunction (De Morgan's law)

pm4.57Theorem *4.57 of WhiteheadRussell p. 120

pm3.1Theorem *3.1 of WhiteheadRussell p. 111

pm3.11Theorem *3.11 of WhiteheadRussell p. 111

pm3.12Theorem *3.12 of WhiteheadRussell p. 111

pm3.13Theorem *3.13 of WhiteheadRussell p. 111

pm3.14Theorem *3.14 of WhiteheadRussell p. 111

pm4.44Theorem *4.44 of WhiteheadRussell p. 119

pm4.45Theorem *4.45 of WhiteheadRussell p. 119

orabsAbsorption of redundant internal disjunct

oranabsAbsorb a disjunct into a conjunct

pm5.61Theorem *5.61 of WhiteheadRussell p. 125

pm5.6Conjunction in antecedent versus disjunction in consequent

orcanaiChange disjunction in consequent to conjunction in antecedent

orsildA lemma for not-or-not elimination, in deduction form

orsirdA lemma for not-or-not elimination, in deduction form

pm4.79Theorem *4.79 of WhiteheadRussell p. 121

pm5.53Theorem *5.53 of WhiteheadRussell p. 125

ordiDistributive law for disjunction

ordirDistributive law for disjunction

andiDistributive law for conjunction

andirDistributive law for conjunction

orddiDouble distributive law for disjunction

anddiDouble distributive law for conjunction

pm5.17Theorem *5.17 of WhiteheadRussell p. 124

pm5.15Theorem *5.15 of WhiteheadRussell p. 124

pm5.16Theorem *5.16 of WhiteheadRussell p. 124

xorTwo ways to express exclusive disjunction ( df-xor )

nbi2Two ways to express "exclusive or"

xordiConjunction distributes over exclusive-or, using -

pm5.54Theorem *5.54 of WhiteheadRussell p. 125

pm5.62Theorem *5.62 of WhiteheadRussell p. 125

pm5.63Theorem *5.63 of WhiteheadRussell p. 125

niabnMiscellaneous inference relating falsehoods

ninbaMiscellaneous inference relating falsehoods

pm4.43Theorem *4.43 of WhiteheadRussell p. 119

pm4.82Theorem *4.82 of WhiteheadRussell p. 122

pm4.83Theorem *4.83 of WhiteheadRussell p. 122

pclem6Negation inferred from embedded conjunct

bigoldenDijkstra-Scholten's Golden Rule for calculational proofs

pm5.71Theorem *5.71 of WhiteheadRussell p. 125

pm5.75Theorem *5.75 of WhiteheadRussell p. 126

ecase2dDeduction for elimination by cases

ecase3Inference for elimination by cases

ecaseInference for elimination by cases

ecase3dDeduction for elimination by cases

ecasedDeduction for elimination by cases

ecase3adDeduction for elimination by cases

ccaseInference for combining cases

ccasedDeduction for combining cases

ccase2Inference for combining cases

4casesInference eliminating two antecedents from the four possible cases that result from their true/false combinations

4casesdanDeduction eliminating two antecedents from the four possible cases that result from their true/false combinations

casesCase disjunction according to the value of ph

dedlem0aLemma for an alternate version of weak deduction theorem

dedlem0bLemma for an alternate version of weak deduction theorem

dedlemaLemma for weak deduction theorem

dedlembLemma for weak deduction theorem

cases2Case disjunction according to the value of ph

cases2ALTAlternate proof of cases2, not using dedlema or dedlemb

dfbi3An alternate definition of the biconditional

pm5.24Theorem *5.24 of WhiteheadRussell p. 124

4exmidThe disjunction of the four possible combinations of two wffs and their negations is always true

consensusThe consensus theorem

pm4.42Theorem *4.42 of WhiteheadRussell p. 119

prlem1A specialized lemma for set theory (to derive the Axiom of Pairing)

prlem2A specialized lemma for set theory (to derive the Axiom of Pairing)

oplem1A specialized lemma for set theory (ordered pair theorem)

dn1A single axiom for Boolean algebra known as DN1

bianirA closed form of mpbir, analogous to pm2.27 (assertion)

jaoi2Inference removing a negated conjunct in a disjunction of an antecedent if this conjunct is part of the disjunction

jaoi3Inference separating a disjunct of an antecedent

ornldSelecting one statement from a disjunction if one of the disjuncted statements is false

The conditional operator for propositions

dfifp2Alternate definition of the conditional operator for propositions

dfifp3Alternate definition of the conditional operator for propositions

dfifp4Alternate definition of the conditional operator for propositions

dfifp5Alternate definition of the conditional operator for propositions

dfifp6Alternate definition of the conditional operator for propositions

dfifp7Alternate definition of the conditional operator for propositions

ifpdfbiDefine the biconditional as conditional logic operator

ifpdfbiOLDObsolete version of ifpdfbi as of 25-Jun-2026

anifpThe conditional operator is implied by the conjunction of its possible outputs

ifporThe conditional operator implies the disjunction of its possible outputs

ifpnConditional operator for the negation of a proposition

ifptruValue of the conditional operator for propositions when its first argument is true

ifpfalValue of the conditional operator for propositions when its first argument is false

ifpidValue of the conditional operator for propositions when the same proposition is returned in either case

casesifpVersion of cases expressed using if-

ifpbi123dEquivalence deduction for conditional operator for propositions

ifpbi23dEquivalence deduction for conditional operator for propositions

ifpimpdaSeparation of the values of the conditional operator for propositions

1fpid3The value of the conditional operator for propositions is its third argument if the first and second argument imply the third argument

The weak deduction theorem for propositional calculus

elimhHypothesis builder for the weak deduction theorem

dedtThe weak deduction theorem

con3ALTProof of con3 from its associated inference con3i that illustrates the use of the weak deduction theorem dedt

Abbreviated conjunction and disjunction of three wff's

3orassAssociative law for triple disjunction

3orel1Partial elimination of a triple disjunction by denial of a disjunct

3orrotRotation law for triple disjunction

3orcomaCommutation law for triple disjunction

3orcombCommutation law for triple disjunction

3anassAssociative law for triple conjunction

3anan12Convert triple conjunction to conjunction, then commute

3anan32Convert triple conjunction to conjunction, then commute

3anan32OLDObsolete version of 3anan32 as of 15-Jun-2026

3ancomaCommutation law for triple conjunction

3ancombCommutation law for triple conjunction

3anrotRotation law for triple conjunction

3anrevReversal law for triple conjunction

anandi3Distribution of triple conjunction over conjunction

anandi3rDistribution of triple conjunction over conjunction

3anidmIdempotent law for conjunction

3an4anassAssociative law for four conjunctions with a triple conjunction

3ioranNegated triple disjunction as triple conjunction

3ianorNegated triple conjunction expressed in terms of triple disjunction

3anorTriple conjunction expressed in terms of triple disjunction

3oranTriple disjunction in terms of triple conjunction

3impaImportation from double to triple conjunction

3impImportation inference

3imp31The importation inference 3imp with commutation of the first and third conjuncts of the assertion relative to the hypothesis

3imp231Importation inference

3imp21The importation inference 3imp with commutation of the first and second conjuncts of the assertion relative to the hypothesis

3impbImportation from double to triple conjunction

bi23imp133imp with middle implication of the hypothesis a biconditional

3impibImportation to triple conjunction

3impiaImportation to triple conjunction

3expaExportation from triple to double conjunction

3expExportation inference

3expbExportation from triple to double conjunction

3expiaExportation from triple conjunction

3expibExportation from triple conjunction

3com12Commutation in antecedent

3com13Commutation in antecedent

3comrCommutation in antecedent

3com23Commutation in antecedent

3comlCommutation in antecedent

3jcaJoin consequents with conjunction

3jcadDeduction conjoining the consequents of three implications

3adant1Deduction adding a conjunct to antecedent

3adant2Deduction adding a conjunct to antecedent

3adant3Deduction adding a conjunct to antecedent

3ad2ant1Deduction adding conjuncts to an antecedent

3ad2ant2Deduction adding conjuncts to an antecedent

3ad2ant3Deduction adding conjuncts to an antecedent

simp1Simplification of triple conjunction

simp2Simplification of triple conjunction

simp3Simplification of triple conjunction

simp1iInfer a conjunct from a triple conjunction

simp2iInfer a conjunct from a triple conjunction

simp3iInfer a conjunct from a triple conjunction

simp1dDeduce a conjunct from a triple conjunction

simp2dDeduce a conjunct from a triple conjunction

simp3dDeduce a conjunct from a triple conjunction

simp1biDeduce a conjunct from a triple conjunction

simp2biDeduce a conjunct from a triple conjunction

simp3biDeduce a conjunct from a triple conjunction

3simpaSimplification of triple conjunction

3simpbSimplification of triple conjunction

3simpcSimplification of triple conjunction

3anim123iJoin antecedents and consequents with conjunction

3anim1iAdd two conjuncts to antecedent and consequent

3anim2iAdd two conjuncts to antecedent and consequent

3anim3iAdd two conjuncts to antecedent and consequent

3anbi123iJoin 3 biconditionals with conjunction

3orbi123iJoin 3 biconditionals with disjunction

3anbi1iInference adding two conjuncts to each side of a biconditional

3anbi2iInference adding two conjuncts to each side of a biconditional

3anbi3iInference adding two conjuncts to each side of a biconditional

syl3anA triple syllogism inference

syl3anbA triple syllogism inference

syl3anbrA triple syllogism inference

syl3an1A syllogism inference

syl3an2A syllogism inference

syl3an3A syllogism inference

syl3an132syl2an with antecedents in standard conjunction form

3adantl1Deduction adding a conjunct to antecedent

3adantl2Deduction adding a conjunct to antecedent

3adantl3Deduction adding a conjunct to antecedent

3adantr1Deduction adding a conjunct to antecedent

3adantr2Deduction adding a conjunct to antecedent

3adantr3Deduction adding a conjunct to antecedent

ad4ant123Deduction adding conjuncts to antecedent

ad4ant124Deduction adding conjuncts to antecedent

ad4ant134Deduction adding conjuncts to antecedent

ad4ant234Deduction adding conjuncts to antecedent

3adant1lDeduction adding a conjunct to antecedent

3adant1rDeduction adding a conjunct to antecedent

3adant2lDeduction adding a conjunct to antecedent

3adant2rDeduction adding a conjunct to antecedent

3adant3lDeduction adding a conjunct to antecedent

3adant3rDeduction adding a conjunct to antecedent

3adant3r1Deduction adding a conjunct to antecedent

3adant3r2Deduction adding a conjunct to antecedent

3adant3r3Deduction adding a conjunct to antecedent

3ad2antl1Deduction adding conjuncts to antecedent

3ad2antl2Deduction adding conjuncts to antecedent

3ad2antl3Deduction adding conjuncts to antecedent

3ad2antr1Deduction adding conjuncts to antecedent

3ad2antr2Deduction adding conjuncts to antecedent

3ad2antr3Deduction adding conjuncts to antecedent

simpl1Simplification of conjunction

simpl2Simplification of conjunction

simpl3Simplification of conjunction

simpr1Simplification of conjunction

simpr2Simplification of conjunction

simpr3Simplification of conjunction

simp1lSimplification of triple conjunction

simp1rSimplification of triple conjunction

simp2lSimplification of triple conjunction

simp2rSimplification of triple conjunction

simp3lSimplification of triple conjunction

simp3rSimplification of triple conjunction

simp11Simplification of doubly triple conjunction

simp12Simplification of doubly triple conjunction

simp13Simplification of doubly triple conjunction

simp21Simplification of doubly triple conjunction

simp22Simplification of doubly triple conjunction

simp23Simplification of doubly triple conjunction

simp31Simplification of doubly triple conjunction

simp32Simplification of doubly triple conjunction

simp33Simplification of doubly triple conjunction

simpll1Simplification of conjunction

simpll2Simplification of conjunction

simpll3Simplification of conjunction

simplr1Simplification of conjunction

simplr2Simplification of conjunction

simplr3Simplification of conjunction

simprl1Simplification of conjunction

simprl2Simplification of conjunction

simprl3Simplification of conjunction

simprr1Simplification of conjunction

simprr2Simplification of conjunction

simprr3Simplification of conjunction

simpl1lSimplification of conjunction

simpl1rSimplification of conjunction

simpl2lSimplification of conjunction

simpl2rSimplification of conjunction

simpl3lSimplification of conjunction

simpl3rSimplification of conjunction

simpr1lSimplification of conjunction

simpr1rSimplification of conjunction

simpr2lSimplification of conjunction

simpr2rSimplification of conjunction

simpr3lSimplification of conjunction

simpr3rSimplification of conjunction

simp1llSimplification of conjunction

simp1lrSimplification of conjunction

simp1rlSimplification of conjunction

simp1rrSimplification of conjunction

simp2llSimplification of conjunction

simp2lrSimplification of conjunction

simp2rlSimplification of conjunction

simp2rrSimplification of conjunction

simp3llSimplification of conjunction

simp3lrSimplification of conjunction

simp3rlSimplification of conjunction

simp3rrSimplification of conjunction

simpl11Simplification of conjunction

simpl12Simplification of conjunction

simpl13Simplification of conjunction

simpl21Simplification of conjunction

simpl22Simplification of conjunction

simpl23Simplification of conjunction

simpl31Simplification of conjunction

simpl32Simplification of conjunction

simpl33Simplification of conjunction

simpr11Simplification of conjunction

simpr12Simplification of conjunction

simpr13Simplification of conjunction

simpr21Simplification of conjunction

simpr22Simplification of conjunction

simpr23Simplification of conjunction

simpr31Simplification of conjunction

simpr32Simplification of conjunction

simpr33Simplification of conjunction

simp1l1Simplification of conjunction

simp1l2Simplification of conjunction

simp1l3Simplification of conjunction

simp1r1Simplification of conjunction

simp1r2Simplification of conjunction

simp1r3Simplification of conjunction

simp2l1Simplification of conjunction

simp2l2Simplification of conjunction

simp2l3Simplification of conjunction

simp2r1Simplification of conjunction

simp2r2Simplification of conjunction

simp2r3Simplification of conjunction

simp3l1Simplification of conjunction

simp3l2Simplification of conjunction

simp3l3Simplification of conjunction

simp3r1Simplification of conjunction

simp3r2Simplification of conjunction

simp3r3Simplification of conjunction

simp11lSimplification of conjunction

simp11rSimplification of conjunction

simp12lSimplification of conjunction

simp12rSimplification of conjunction

simp13lSimplification of conjunction

simp13rSimplification of conjunction

simp21lSimplification of conjunction

simp21rSimplification of conjunction

simp22lSimplification of conjunction

simp22rSimplification of conjunction

simp23lSimplification of conjunction

simp23rSimplification of conjunction

simp31lSimplification of conjunction

simp31rSimplification of conjunction

simp32lSimplification of conjunction

simp32rSimplification of conjunction

simp33lSimplification of conjunction

simp33rSimplification of conjunction

simp111Simplification of conjunction

simp112Simplification of conjunction

simp113Simplification of conjunction

simp121Simplification of conjunction

simp122Simplification of conjunction

simp123Simplification of conjunction

simp131Simplification of conjunction

simp132Simplification of conjunction

simp133Simplification of conjunction

simp211Simplification of conjunction

simp212Simplification of conjunction

simp213Simplification of conjunction

simp221Simplification of conjunction

simp222Simplification of conjunction

simp223Simplification of conjunction

simp231Simplification of conjunction

simp232Simplification of conjunction

simp233Simplification of conjunction

simp311Simplification of conjunction

simp312Simplification of conjunction

simp313Simplification of conjunction

simp321Simplification of conjunction

simp322Simplification of conjunction

simp323Simplification of conjunction

simp331Simplification of conjunction

simp332Simplification of conjunction

simp333Simplification of conjunction

3anibarRemove a hypothesis from the second member of a biconditional

3mix1Introduction in triple disjunction

3mix2Introduction in triple disjunction

3mix3Introduction in triple disjunction

3mix1iIntroduction in triple disjunction

3mix2iIntroduction in triple disjunction

3mix3iIntroduction in triple disjunction

3mix1dDeduction introducing triple disjunction

3mix2dDeduction introducing triple disjunction

3mix3dDeduction introducing triple disjunction

3pm3.2iInfer conjunction of premises

pm3.2an3Version of pm3.2 for a triple conjunction

mpbir3anDetach a conjunction of truths in a biconditional

mpbir3andDetach a conjunction of truths in a biconditional

syl3anbrcSyllogism inference

syl21anbrcSyllogism inference

3imp3i2anAn elimination deduction

ex3Apply ex to a hypothesis with a 3-right-nested conjunction antecedent, with the antecedent of the assertion being a triple conjunction rather than a 2-right-nested conjunction

3imp1Importation to left triple conjunction

3impdImportation deduction for triple conjunction

3imp2Importation to right triple conjunction

3impdiImportation inference (undistribute conjunction)

3impdirImportation inference (undistribute conjunction)

3exp1Exportation from left triple conjunction

3expdExportation deduction for triple conjunction

3exp2Exportation from right triple conjunction

exp5oA triple exportation inference

exp516A triple exportation inference

exp520A triple exportation inference

3impexpVersion of impexp for a triple conjunction

3an1rsSwap conjuncts

13an22anassAssociative law for four conjunctions with a triple conjunction

3anasssAssociative law for conjunction applied to antecedent (eliminates syllogism)

3anassrsAssociative law for conjunction applied to antecedent (eliminates syllogism)

4anpull2An equivalence of two four-terms conjunctions with the terms regrouped (here, the second sub-conjunct of the first term is pulled separately)

4anpull2OLDObsolete version of 4anpull2 as of 26-Jun-2026

ad5ant245Deduction adding conjuncts to antecedent

ad5ant234Deduction adding conjuncts to antecedent

ad5ant235Deduction adding conjuncts to antecedent

ad5ant123Deduction adding conjuncts to antecedent

ad5ant124Deduction adding conjuncts to antecedent

ad5ant124OLDObsolete version of ad5ant124 as of 13-Jun-2026

ad5ant125Deduction adding conjuncts to antecedent

ad5ant125OLDObsolete version of ad5ant125 as of 13-Jun-2026

ad5ant134Deduction adding conjuncts to antecedent

ad5ant134OLDObsolete version of ad5ant134 as of 13-Jun-2026

ad5ant135Deduction adding conjuncts to antecedent

ad5ant135OLDObsolete version of ad5ant135 as of 13-Jun-2026

ad5ant145Deduction adding conjuncts to antecedent

ad5ant2345Deduction adding conjuncts to antecedent

syl3ancSyllogism combined with contraction

syl13ancSyllogism combined with contraction

syl31ancSyllogism combined with contraction

syl112ancSyllogism combined with contraction

syl121ancSyllogism combined with contraction

syl211ancSyllogism combined with contraction

syl23ancSyllogism combined with contraction

syl32ancSyllogism combined with contraction

syl122ancSyllogism combined with contraction

syl212ancSyllogism combined with contraction

syl221ancSyllogism combined with contraction

syl113ancSyllogism combined with contraction

syl131ancSyllogism combined with contraction

syl311ancSyllogism combined with contraction

syl33ancSyllogism combined with contraction

syl222ancSyllogism combined with contraction

syl123ancSyllogism combined with contraction

syl132ancSyllogism combined with contraction

syl213ancSyllogism combined with contraction

syl231ancSyllogism combined with contraction

syl312ancSyllogism combined with contraction

syl321ancSyllogism combined with contraction

syl133ancSyllogism combined with contraction

syl313ancSyllogism combined with contraction

syl331ancSyllogism combined with contraction

syl223ancSyllogism combined with contraction

syl232ancSyllogism combined with contraction

syl322ancSyllogism combined with contraction

syl233ancSyllogism combined with contraction

syl323ancSyllogism combined with contraction

syl332ancSyllogism combined with contraction

syl333ancA syllogism inference combined with contraction

syl3an1bA syllogism inference

syl3an2bA syllogism inference

syl3an3bA syllogism inference

syl3an1brA syllogism inference

syl3an2brA syllogism inference

syl3an3brA syllogism inference

syld3an3A syllogism inference

syld3an1A syllogism inference

syld3an2A syllogism inference

syl3anl1A syllogism inference

syl3anl2A syllogism inference

syl3anl3A syllogism inference

syl3anlA triple syllogism inference

syl3anr1A syllogism inference

syl3anr2A syllogism inference

syl3anr3A syllogism inference

3anidm12Inference from idempotent law for conjunction

3anidm13Inference from idempotent law for conjunction

3anidm23Inference from idempotent law for conjunction

syl2an3ansyl3an with antecedents in standard conjunction form

syl2an23anDeduction related to syl3an with antecedents in standard conjunction form

3oriInfer implication from triple disjunction

3jaoDisjunction of three antecedents

3jaobDisjunction of three antecedents

3jaoiDisjunction of three antecedents (inference)

3jaoiOLDObsolete version of 3jaoi as of 16-Jun-2026

3jaodDisjunction of three antecedents (deduction)

3jaoianDisjunction of three antecedents (inference)

3jaodanDisjunction of three antecedents (deduction)

mpjao3danEliminate a three-way disjunction in a deduction

3jaaoInference conjoining and disjoining the antecedents of three implications

3jaaoOLDObsolete version of 3jaao as of 16-Jun-2026

syl3an9bNested syllogism inference conjoining 3 dissimilar antecedents

3orbi123dDeduction joining 3 equivalences to form equivalence of disjunctions

3anbi123dDeduction joining 3 equivalences to form equivalence of conjunctions

3anbi12dDeduction conjoining and adding a conjunct to equivalences

3anbi13dDeduction conjoining and adding a conjunct to equivalences

3anbi23dDeduction conjoining and adding a conjunct to equivalences

3anbi1dDeduction adding conjuncts to an equivalence

3anbi2dDeduction adding conjuncts to an equivalence

3anbi3dDeduction adding conjuncts to an equivalence

3anim123dDeduction joining 3 implications to form implication of conjunctions

3orim123dDeduction joining 3 implications to form implication of disjunctions

3orim123daDisjoin antecedents and consequents of three premises

an6Rearrangement of 6 conjuncts

3an6Analogue of an4 for triple conjunction

3or6Analogue of or4 for triple conjunction

mp3an1An inference based on modus ponens

mp3an2An inference based on modus ponens

mp3an3An inference based on modus ponens

mp3an12An inference based on modus ponens

mp3an13An inference based on modus ponens

mp3an23An inference based on modus ponens

mp3an1iAn inference based on modus ponens

mp3anl1An inference based on modus ponens

mp3anl2An inference based on modus ponens

mp3anl3An inference based on modus ponens

mp3anr1An inference based on modus ponens

mp3anr2An inference based on modus ponens

mp3anr3An inference based on modus ponens

mp3anAn inference based on modus ponens

mpd3an3An inference based on modus ponens

mpd3an23An inference based on modus ponens

mp3andA deduction based on modus ponens

mp3an12imp3an with antecedents in standard conjunction form and with one hypothesis an implication

mp3an2imp3an with antecedents in standard conjunction form and with two hypotheses which are implications

mp3an3anmp3an with antecedents in standard conjunction form and with two hypotheses which are implications

mp3an2aniAn elimination deduction

biimp3aInfer implication from a logical equivalence

biimp3arInfer implication from a logical equivalence

3anandisInference that undistributes a triple conjunction in the antecedent

3anandirsInference that undistributes a triple conjunction in the antecedent

ecase13dDeduction for elimination by cases

ecase23dDeduction for elimination by cases

ecase33dDeduction for elimination by cases

3ecaseInference for elimination by cases

3bior1fdA disjunction is equivalent to a threefold disjunction with single falsehood, analogous to biorf

3bior1fandA disjunction is equivalent to a threefold disjunction with single falsehood of a conjunction

3bior2fdA wff is equivalent to its threefold disjunction with double falsehood, analogous to biorf

3biant1dA conjunction is equivalent to a threefold conjunction with single truth, analogous to biantrud

intn3an1dIntroduction of a triple conjunct inside a contradiction

intn3an2dIntroduction of a triple conjunct inside a contradiction

intn3an3dIntroduction of a triple conjunct inside a contradiction

an3andiDistribution of conjunction over threefold conjunction

an33reanRearrange a 9-fold conjunction

3orel2Partial elimination of a triple disjunction by denial of a disjunct

3orel3Partial elimination of a triple disjunction by denial of a disjunct

3orel13Elimination of two disjuncts in a triple disjunction

3pm3.2niTriple negated disjunction introduction

an42dsInference exchanging the last antecedent with the second one

Logical "nand" (Sheffer stroke)

nananConjunction in terms of alternative denial

dfnan2Alternative denial in terms of our primitive connectives (implication and negation)

nanorAlternative denial in terms of disjunction and negation

nancomAlternative denial is commutative

nannanNested alternative denials

nanimImplication in terms of alternative denial

nannotNegation in terms of alternative denial

nanbiBiconditional in terms of alternative denial

nanbi1Introduce a right anti-conjunct to both sides of a logical equivalence

nanbi2Introduce a left anti-conjunct to both sides of a logical equivalence

nanbi12Join two logical equivalences with anti-conjunction

nanbi1iIntroduce a right anti-conjunct to both sides of a logical equivalence

nanbi2iIntroduce a left anti-conjunct to both sides of a logical equivalence

nanbi12iJoin two logical equivalences with anti-conjunction

nanbi1dIntroduce a right anti-conjunct to both sides of a logical equivalence

nanbi2dIntroduce a left anti-conjunct to both sides of a logical equivalence

nanbi12dJoin two logical equivalences with anti-conjunction

nanassA characterization of when an expression involving alternative denials associates

Logical "xor"

xnorTwo ways to write XNOR (exclusive not-or)

xorcomThe connector \/_ is commutative

xorassThe connector \/_ is associative

excxorThis tautology shows that xor is really exclusive

xor2Two ways to express "exclusive or"

xororExclusive disjunction implies disjunction ("XOR implies OR")

xornanExclusive disjunction implies alternative denial ("XOR implies NAND")

xornan2XOR implies NAND (written with the -/\ connector)

xorneg2The connector \/_ is negated under negation of one argument

xorneg1The connector \/_ is negated under negation of one argument

xornegThe connector \/_ is unchanged under negation of both arguments

xorbi12iEquality property for exclusive disjunction

xorbi12dEquality property for exclusive disjunction

anxordiConjunction distributes over exclusive-or

xorexmidExclusive-or variant of the law of the excluded middle ( exmid )

Logical "nor"

norcomThe connector -\/ is commutative

noran/\ is expressible via -\/

noror\/ is expressible via -\/

norasslem1This lemma shows the equivalence of two expressions, used in norass

norasslem2This lemma specializes biimt suitably for the proof of norass

norasslem3This lemma specializes biorf suitably for the proof of norass

norassA characterization of when an expression involving joint denials associates

True and false constants

The true constant

trujustSoundness justification theorem for df-tru

truThe truth value wtru is provable

dftru2An alternate definition of "true" (see comment of df-tru )

trutA proposition is equivalent to it being implied by wtru

mptruEliminate wtru as an antecedent

tbtruA proposition is equivalent to itself being equivalent to wtru

bitruA theorem is equivalent to truth

trudAnything implies wtru

truanTrue can be removed from a conjunction

The false constant

falThe truth value wfal is refutable

nbfalThe negation of a proposition is equivalent to itself being equivalent to wfal

bifalA contradiction is equivalent to falsehood

falimThe truth value wfal implies anything

falimdThe truth value wfal implies anything

dfnotGiven falsum wfal, we can define the negation of a wff ph as the statement that wfal follows from assuming ph

inegdNegation introduction rule from natural deduction

efaldDeduction based on reductio ad absurdum

pm2.21falIf a wff and its negation are provable, then falsum is provable

Truth tables

Implication

truimtruA -> identity

truimfalA -> identity

falimtruA -> identity

falimfalA -> identity

Negation

Equivalence

trubitruA <-> identity

falbitruA <-> identity

trubifalA <-> identity

falbifalA <-> identity

Conjunction

truantruA /\ identity

truanfalA /\ identity

falantruA /\ identity

falanfalA /\ identity

Disjunction

truortruA \/ identity

truorfalA \/ identity

falortruA \/ identity

falorfalA \/ identity

Alternative denial

trunantruA -/\ identity

trunanfalA -/\ identity

falnantruA -/\ identity

falnanfalA -/\ identity

Exclusive disjunction

truxortruA \/_ identity

truxorfalA \/_ identity

falxortruA \/_ identity

falxorfalA \/_ identity

Joint denial

trunortruA -\/ identity

trunorfalA -\/ identity

falnortruA -\/ identity

falnorfalA -\/ identity

Half adder and full adder in propositional calculus

Full adder: sum

hadbi123dEquality theorem for the adder sum

hadbi123iEquality theorem for the adder sum

hadassAssociative law for the adder sum

hadbiThe adder sum is the same as the triple biconditional

hadcomaCommutative law for the adder sum

hadcombCommutative law for the adders sum

hadrotRotation law for the adder sum

hadnotThe adder sum distributes over negation

had1If the first input is true, then the adder sum is equivalent to the biconditionality of the other two inputs, and conversely

had0If the first input is false, then the adder sum is equivalent to the exclusive disjunction of the other two inputs, and conversely

had1OLDObsolete version of had1 as of 10-Aug-2026

had0OLDObsolete version of had0 as of 10-Aug-2026

hadifpThe value of the adder sum is, if the first input is true, the biconditionality, and if the first input is false, the exclusive disjunction, of the other two inputs

hadifpOLDObsolete version of hadifp as of 10-Aug-2026

Full adder: carry

cadorThe adder carry in disjunctive normal form

cadanThe adder carry in conjunctive normal form

cadbi123dEquality theorem for the adder carry

cadbi123iEquality theorem for the adder carry

cadcomaCommutative law for the adder carry

cadcombCommutative law for the adder carry

cadrotRotation law for the adder carry

cadnotThe adder carry distributes over negation

cad11If (at least) two inputs are true, then the adder carry is true

cad1If one input is true, then the adder carry is true exactly when at least one of the other two inputs is true

cad0If one input is false, then the adder carry is true exactly when both of the other two inputs are true

cadifpThe value of the carry is, if the input carry is true, the disjunction, and if the input carry is false, the conjunction, of the other two inputs

cadtruThe adder carry is true as soon as its first two inputs are the truth constant

Other axiomatizations related to classical propositional calculus

Minimal implicational calculus

minimpA single axiom for minimal implicational calculus, due to Meredith

minimp-syllsimpDerivation of Syll-Simp ( jarr) from ax-mp and minimp

minimp-ax1Derivation of ax-1 from ax-mp and minimp

minimp-ax2cDerivation of a commuted form of ax-2 from ax-mp and minimp

minimp-ax2Derivation of ax-2 from ax-mp and minimp

minimp-pm2.43Derivation of pm2.43 (also called "hilbert" or W) from ax-mp and minimp

Implicational Calculus

impsingleThe shortest single axiom for implicational calculus, due to Lukasiewicz

impsingle-step4Derivation of impsingle-step4 from ax-mp and impsingle

impsingle-step8Derivation of impsingle-step8 from ax-mp and impsingle

impsingle-ax1Derivation of impsingle-ax1 ( ax-1) from ax-mp and impsingle

impsingle-step15Derivation of impsingle-step15 from ax-mp and impsingle

impsingle-step18Derivation of impsingle-step18 from ax-mp and impsingle

impsingle-step19Derivation of impsingle-step19 from ax-mp and impsingle

impsingle-step20Derivation of impsingle-step20 from ax-mp and impsingle

impsingle-step21Derivation of impsingle-step21 from ax-mp and impsingle

impsingle-step22Derivation of impsingle-step22 from ax-mp and impsingle

impsingle-step25Derivation of impsingle-step25 from ax-mp and impsingle

impsingle-imim1Derivation of impsingle-imim1 ( imim1) from ax-mp and impsingle

impsingle-peirceDerivation of impsingle-peirce ( peirce) from ax-mp and impsingle

tarski-bernays-ax2Derivation of ax-2 from the Tarski-Bernays axiom set { ax-1, imim1, peirce }

Derive the Lukasiewicz axioms from Meredith's sole axiom

meredithCarew Meredith's sole axiom for propositional calculus

merlem1Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom

merlem2Step 4 of Meredith's proof of Lukasiewicz axioms from his sole axiom

merlem3Step 7 of Meredith's proof of Lukasiewicz axioms from his sole axiom

merlem4Step 8 of Meredith's proof of Lukasiewicz axioms from his sole axiom

merlem5Step 11 of Meredith's proof of Lukasiewicz axioms from his sole axiom

merlem6Step 12 of Meredith's proof of Lukasiewicz axioms from his sole axiom

merlem7Between steps 14 and 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom

merlem8Step 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom

merlem9Step 18 of Meredith's proof of Lukasiewicz axioms from his sole axiom

merlem10Step 19 of Meredith's proof of Lukasiewicz axioms from his sole axiom

merlem11Step 20 of Meredith's proof of Lukasiewicz axioms from his sole axiom

merlem12Step 28 of Meredith's proof of Lukasiewicz axioms from his sole axiom

merlem13Step 35 of Meredith's proof of Lukasiewicz axioms from his sole axiom

luk-11 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom

luk-22 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom

luk-33 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom

Derive the standard axioms from the Lukasiewicz axioms

luklem1Used to rederive standard propositional axioms from Lukasiewicz'

luklem2Used to rederive standard propositional axioms from Lukasiewicz'

luklem3Used to rederive standard propositional axioms from Lukasiewicz'

luklem4Used to rederive standard propositional axioms from Lukasiewicz'

luklem5Used to rederive standard propositional axioms from Lukasiewicz'

luklem6Used to rederive standard propositional axioms from Lukasiewicz'

luklem7Used to rederive standard propositional axioms from Lukasiewicz'

luklem8Used to rederive standard propositional axioms from Lukasiewicz'

ax1Standard propositional axiom derived from Lukasiewicz axioms

ax2Standard propositional axiom derived from Lukasiewicz axioms

ax3Standard propositional axiom derived from Lukasiewicz axioms

Derive Nicod's axiom from the standard axioms

nic-dfimThis theorem "defines" implication in terms of 'nand'

nic-dfnegThis theorem "defines" negation in terms of 'nand'

nic-mpDerive Nicod's rule of modus ponens using 'nand', from the standard one

nic-mpALTA direct proof of nic-mp

nic-axNicod's axiom derived from the standard ones

nic-axALTA direct proof of nic-ax

Derive the Lukasiewicz axioms from Nicod's axiom

nic-impInference for nic-mp using nic-ax as major premise

nic-idlem1Lemma for nic-id

nic-idlem2Lemma for nic-id

nic-idTheorem id expressed with -/\

nic-swapThe connector -/\ is symmetric

nic-isw1Inference version of nic-swap

nic-isw2Inference for swapping nested terms

nic-iimp1Inference version of nic-imp using right-handed term

nic-iimp2Inference version of nic-imp using left-handed term

nic-idelInference to remove the trailing term

nic-ichChained inference

nic-idblDouble the terms

nic-bijustBiconditional justification from Nicod's axiom

nic-bi1Inference to extract one side of an implication from a definition

nic-bi2Inference to extract the other side of an implication from a 'biconditional' definition

nic-stdmpDerive the standard modus ponens from nic-mp

nic-luk1Proof of luk-1 from nic-ax and nic-mp (and Definitions nic-dfim and nic-dfneg )

nic-luk2Proof of luk-2 from nic-ax and nic-mp

nic-luk3Proof of luk-3 from nic-ax and nic-mp

Derive Nicod's Axiom from Lukasiewicz's First Sheffer Stroke Axiom

lukshef-ax1This alternative axiom for propositional calculus using the Sheffer Stroke was discovered by Lukasiewicz in his Selected Works

lukshefth1Lemma for renicax

lukshefth2Lemma for renicax

renicaxA rederivation of nic-ax from lukshef-ax1, proving that lukshef-ax1 with nic-mp can be used as a complete axiomatization of propositional calculus

Derive the Lukasiewicz Axioms from the Tarski-Bernays-Wajsberg Axioms

tbw-bijustJustification for tbw-negdf

tbw-negdfThe definition of negation, in terms of -> and wfal

tbw-ax1The first of four axioms in the Tarski-Bernays-Wajsberg system

tbw-ax2The second of four axioms in the Tarski-Bernays-Wajsberg system

tbw-ax3The third of four axioms in the Tarski-Bernays-Wajsberg system

tbw-ax4The fourth of four axioms in the Tarski-Bernays-Wajsberg system

tbwsylUsed to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'

tbwlem1Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'

tbwlem2Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'

tbwlem3Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'

tbwlem4Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'

tbwlem5Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'

re1luk1luk-1 derived from the Tarski-Bernays-Wajsberg axioms

re1luk2luk-2 derived from the Tarski-Bernays-Wajsberg axioms

re1luk3luk-3 derived from the Tarski-Bernays-Wajsberg axioms

Derive the Tarski-Bernays-Wajsberg axioms from Meredith's First CO Axiom

merco1A single axiom for propositional calculus discovered by C

merco1lem1Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

retbwax4tbw-ax4 rederived from merco1

retbwax2tbw-ax2 rederived from merco1

merco1lem2Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem3Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem4Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem5Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem6Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem7Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

retbwax3tbw-ax3 rederived from merco1

merco1lem8Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem9Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem10Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem11Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem12Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem13Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem14Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem15Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem16Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem17Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

merco1lem18Used to rederive the Tarski-Bernays-Wajsberg axioms from merco1

retbwax1tbw-ax1 rederived from merco1

Derive the Tarski-Bernays-Wajsberg axioms from Meredith's Second CO Axiom

merco2A single axiom for propositional calculus discovered by C

mercolem1Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2

mercolem2Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2

mercolem3Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2

mercolem4Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2

mercolem5Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2

mercolem6Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2

mercolem7Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2

mercolem8Used to rederive the Tarski-Bernays-Wajsberg axioms from merco2

re1tbw1tbw-ax1 rederived from merco2

re1tbw2tbw-ax2 rederived from merco2

re1tbw3tbw-ax3 rederived from merco2

re1tbw4tbw-ax4 rederived from merco2

Derive the Lukasiewicz axioms from the Russell-Bernays Axioms

rb-bijustJustification for rb-imdf

rb-imdfThe definition of implication, in terms of \/ and -.

anmpModus ponens for { \/ , -

rb-ax1The first of four axioms in the Russell-Bernays axiom system

rb-ax2The second of four axioms in the Russell-Bernays axiom system

rb-ax3The third of four axioms in the Russell-Bernays axiom system

rb-ax4The fourth of four axioms in the Russell-Bernays axiom system

rbsylUsed to rederive the Lukasiewicz axioms from Russell-Bernays'

rblem1Used to rederive the Lukasiewicz axioms from Russell-Bernays'

rblem2Used to rederive the Lukasiewicz axioms from Russell-Bernays'

rblem3Used to rederive the Lukasiewicz axioms from Russell-Bernays'

rblem4Used to rederive the Lukasiewicz axioms from Russell-Bernays'

rblem5Used to rederive the Lukasiewicz axioms from Russell-Bernays'

rblem6Used to rederive the Lukasiewicz axioms from Russell-Bernays'

rblem7Used to rederive the Lukasiewicz axioms from Russell-Bernays'

re1axmpax-mp derived from Russell-Bernays'

re2luk1luk-1 derived from Russell-Bernays'

re2luk2luk-2 derived from Russell-Bernays'

re2luk3luk-3 derived from Russell-Bernays'

Stoic logic non-modal portion (Chrysippus of Soli)

mptnanModus ponendo tollens 1, one of the "indemonstrables" in Stoic logic

mptxorModus ponendo tollens 2, one of the "indemonstrables" in Stoic logic

mtporModus tollendo ponens (inclusive-or version), aka disjunctive syllogism

mtpxorModus tollendo ponens (original exclusive-or version), aka disjunctive syllogism, similar to mtpor, one of the five "indemonstrables" in Stoic logic

stoic1aStoic logic Thema 1 (part a)

stoic1bStoic logic Thema 1 (part b)

stoic2aStoic logic Thema 2 version a

stoic2bStoic logic Thema 2 version b

stoic3Stoic logic Thema 3

stoic4aStoic logic Thema 4 version a

stoic4bStoic logic Thema 4 version b

Predicate calculus with equality: Tarski's system S2 (1 rule, 6 schemes)

Universal quantifier (continued); define "exists" and "not free"

Existential quantifier

alnexUniversal quantification of negation is equivalent to negation of existential quantification

eximalAn equivalence between an implication with an existentially quantified antecedent and an implication with a universally quantified consequent

Nonfreeness predicate

nf2Alternate definition of nonfreeness

nf3Alternate definition of nonfreeness

nf4Alternate definition of nonfreeness

nfiDeduce that x is not free in ph from the definition

nfriConsequence of the definition of not-free

nfdDeduce that x is not free in ps in a context

nfrdConsequence of the definition of not-free in a context

nfthtClosed form of nfth

nfnthtClosed form of nfnth

nfntht2Closed form of nfnth

Rule scheme ax-gen (Generalization)

gen2Generalization applied twice

mpgModus ponens combined with generalization

mpgbiModus ponens on biconditional combined with generalization

mpgbirModus ponens on biconditional combined with generalization

nexGeneralization rule for negated wff

nfthNo variable is (effectively) free in a theorem

nfnthNo variable is (effectively) free in a non-theorem

hbthNo variable is (effectively) free in a theorem

nftruThe true constant has no free variables

nffalThe false constant has no free variables (see nftru )

sptruwVersion of sp when ph is true

altruFor all sets, wtru is true

alfalFor all sets, -

Axiom scheme ax-4 (Quantified Implication)

alimRestatement of Axiom ax-4, for labeling consistency

alimiInference quantifying both antecedent and consequent

2alimiInference doubly quantifying both antecedent and consequent

ala1Add an antecedent in a universally quantified formula

al2imClosed form of al2imi

al2imiInference quantifying antecedent, nested antecedent, and consequent

alanimiVariant of al2imi with conjunctive antecedent

alimdhDeduction form of Theorem 19.20 of Margaris p. 90, see alim

albiTheorem 19.15 of Margaris p. 90

albiiInference adding universal quantifier to both sides of an equivalence

2albiiInference adding two universal quantifiers to both sides of an equivalence

3albiiInference adding three universal quantifiers to both sides of an equivalence

sylgtClosed form of sylg

sylgA syllogism combined with generalization

alrimihInference form of Theorem 19.21 of Margaris p. 90

hbxfrbiA utility lemma to transfer a bound-variable hypothesis builder into a definition

alexUniversal quantifier in terms of existential quantifier and negation

exnalExistential quantification of negation is equivalent to negation of universal quantification

2nalexnPart of theorem *11.5 in WhiteheadRussell p. 164

2exnalnTheorem *11.22 in WhiteheadRussell p. 160

2nexalnTheorem *11.25 in WhiteheadRussell p. 160

alimexAn equivalence between an implication with a universally quantified consequent and an implication with an existentially quantified antecedent

aleximiA variant of al2imi: instead of applying A

alexbiiBiconditional form of aleximi

eximTheorem 19.22 of Margaris p. 90

eximiInference adding existential quantifier to antecedent and consequent

2eximiInference adding two existential quantifiers to antecedent and consequent

eximiiInference associated with eximi

exa1Add an antecedent in an existentially quantified formula

19.38Theorem 19.38 of Margaris p. 90

19.38aUnder a nonfreeness hypothesis, the implication 19.38 can be strengthened to an equivalence

19.38bUnder a nonfreeness hypothesis, the implication 19.38 can be strengthened to an equivalence

imnangQuantified implication in terms of quantified negation of conjunction

alinexaA transformation of quantifiers and logical connectives

exnalimnExistential quantification of a conjunction expressed with only primitive symbols ( ->, -., A

alexnA relationship between two quantifiers and negation

2exnexnTheorem *11.51 in WhiteheadRussell p. 164

exbiTheorem 19.18 of Margaris p. 90

exbiiInference adding existential quantifier to both sides of an equivalence

2exbiiInference adding two existential quantifiers to both sides of an equivalence

3exbiiInference adding three existential quantifiers to both sides of an equivalence

nfbiitEquivalence theorem for the nonfreeness predicate

nfbiiEquality theorem for the nonfreeness predicate

nfxfrA utility lemma to transfer a bound-variable hypothesis builder into a definition

nfxfrdA utility lemma to transfer a bound-variable hypothesis builder into a definition

nfnbiA variable is nonfree in a proposition if and only if it is so in its negation

nfntIf a variable is nonfree in a proposition, then it is nonfree in its negation

nfnInference associated with nfnt

nfndDeduction associated with nfnt

exanaliA transformation of quantifiers and logical connectives

2exanaliTheorem *11.521 in WhiteheadRussell p. 164

exancomCommutation of conjunction inside an existential quantifier

exanPlace a conjunct in the scope of an existential quantifier

alrimdhDeduction form of Theorem 19.21 of Margaris p. 90, see 19.21 and 19.21h

eximdhDeduction from Theorem 19.22 of Margaris p. 90

nexdhDeduction for generalization rule for negated wff

albidhFormula-building rule for universal quantifier (deduction form)

exbidhFormula-building rule for existential quantifier (deduction form)

exsimplSimplification of an existentially quantified conjunction

exsimprSimplification of an existentially quantified conjunction

19.26Theorem 19.26 of Margaris p. 90

19.26-2Theorem 19.26 with two quantifiers

19.26-3anTheorem 19.26 with triple conjunction

hbanIf x is not free in ph and ps, it is not free in ph /\ ps

hb3anIf x is not free in ph, ps, and ch, it is not free in w3a ph ps ch

19.29Theorem 19.29 of Margaris p. 90

19.29rVariation of 19.29

19.29r2Variation of 19.29r with double quantification

19.29xVariation of 19.29 with mixed quantification

19.35Theorem 19.35 of Margaris p. 90

19.35iInference associated with 19.35

19.35riInference associated with 19.35

19.25Theorem 19.25 of Margaris p. 90

19.30Theorem 19.30 of Margaris p. 90

19.43Theorem 19.43 of Margaris p. 90

19.43OLDObsolete proof of 19.43

19.33Theorem 19.33 of Margaris p. 90

19.33bThe antecedent provides a condition implying the converse of 19.33

19.40Theorem 19.40 of Margaris p. 90

19.40-2Theorem *11.42 in WhiteheadRussell p. 163

19.40bThe antecedent provides a condition implying the converse of 19.40

albiimSplit a biconditional and distribute quantifier

2albiimSplit a biconditional and distribute two quantifiers

exintrbiAdd/remove a conjunct in the scope of an existential quantifier

exintrIntroduce a conjunct in the scope of an existential quantifier

alsylUniversally quantified and uncurried (imported) form of syllogism

nfimdIf in a context x is not free in ps and ch, then it is not free in ps -> ch

nfimtClosed form of nfim and nfimd

nfimIf x is not free in ph and ps, then it is not free in ph -> ps

nfandIf in a context x is not free in ps and ch, then it is not free in ps /\ ch

nf3andDeduction form of bound-variable hypothesis builder nf3an

nfanIf x is not free in ph and ps, then it is not free in ph /\ ps

nfnanIf x is not free in ph and ps, then it is not free in wnan ph ps

nf3anIf x is not free in ph, ps, and ch, then it is not free in w3a ph ps ch

nfbidIf in a context x is not free in ps and ch, then it is not free in ps <-> ch

nfbiIf x is not free in ph and ps, then it is not free in ph <-> ps

nforIf x is not free in ph and ps, then it is not free in ph \/ ps

nf3orIf x is not free in ph, ps, and ch, then it is not free in w3o ph ps ch

The empty domain of discourse

emptyTwo characterizations of the empty domain

emptyexOn the empty domain, any existentially quantified formula is false

emptyalOn the empty domain, any universally quantified formula is true

emptynfOn the empty domain, any variable is effectively nonfree in any formula

Axiom scheme ax-5 (Distinctness) - first use of $d

ax5dVersion of ax-5 with antecedent

ax5eA rephrasing of ax-5 using the existential quantifier

ax5eaIf a formula holds for some value of a variable not occurring in it, then it holds for all values of that variable

nfvIf x is not present in ph, then x is not free in ph

nfvdnfv with antecedent

alimdvDeduction form of Theorem 19.20 of Margaris p. 90, see alim

eximdvDeduction form of Theorem 19.22 of Margaris p. 90, see exim

2alimdvDeduction form of Theorem 19.20 of Margaris p. 90 with two quantifiers, see alim

2eximdvDeduction form of Theorem 19.22 of Margaris p. 90 with two quantifiers, see exim

albidvFormula-building rule for universal quantifier (deduction form)

exbidvFormula-building rule for existential quantifier (deduction form)

nfbidvAn equality theorem for nonfreeness

2albidvFormula-building rule for two universal quantifiers (deduction form)

2exbidvFormula-building rule for two existential quantifiers (deduction form)

3exbidvFormula-building rule for three existential quantifiers (deduction form)

4exbidvFormula-building rule for four existential quantifiers (deduction form)

alrimivInference form of Theorem 19.21 of Margaris p. 90

alrimivvInference form of Theorem 19.21 of Margaris p. 90

alrimdvDeduction form of Theorem 19.21 of Margaris p. 90

exlimivInference form of Theorem 19.23 of Margaris p. 90, see 19.23

exlimiivInference (Rule C) associated with exlimiv

exlimivvInference form of Theorem 19.23 of Margaris p. 90, see 19.23

exlimdvDeduction form of Theorem 19.23 of Margaris p. 90, see 19.23

exlimdvvDeduction form of Theorem 19.23 of Margaris p. 90, see 19.23

exlimddvExistential elimination rule of natural deduction (Rule C, explained in exlimiv )

nexdvDeduction for generalization rule for negated wff

2ax5Quantification of two variables over a formula in which they do not occur

stdpc5vVersion of stdpc5 with a disjoint variable condition, requiring fewer axioms

19.21vVersion of 19.21 with a disjoint variable condition, requiring fewer axioms

19.32vVersion of 19.32 with a disjoint variable condition, requiring fewer axioms

19.31vVersion of 19.31 with a disjoint variable condition, requiring fewer axioms

19.23vVersion of 19.23 with a disjoint variable condition instead of a nonfreeness hypothesis

19.23vvTheorem 19.23v extended to two variables

pm11.53vVersion of pm11.53 with a disjoint variable condition, requiring fewer axioms

19.36imvOne direction of 19.36v that can be proven without ax-6

19.36ivInference associated with 19.36v

19.37imvOne direction of 19.37v that can be proven without ax-6

19.37ivInference associated with 19.37v

19.41vVersion of 19.41 with a disjoint variable condition, requiring fewer axioms

19.41vvVersion of 19.41 with two quantifiers and a disjoint variable condition requiring fewer axioms

19.41vvvVersion of 19.41 with three quantifiers and a disjoint variable condition requiring fewer axioms

19.41vvvvVersion of 19.41 with four quantifiers and a disjoint variable condition requiring fewer axioms

19.42vVersion of 19.42 with a disjoint variable condition requiring fewer axioms

exdistrDistribution of existential quantifiers

exdistrvDistribute a pair of existential quantifiers (over disjoint variables) over a conjunction

4exdistrvDistribute two pairs of existential quantifiers (over disjoint variables) over a conjunction

19.42vvVersion of 19.42 with two quantifiers and a disjoint variable condition requiring fewer axioms

exdistr2Distribution of existential quantifiers

19.42vvvVersion of 19.42 with three quantifiers and a disjoint variable condition requiring fewer axioms

3exdistrDistribution of existential quantifiers in a triple conjunction

4exdistrDistribution of existential quantifiers in a quadruple conjunction

Equality predicate (continued)

speimfwSpecialization, with additional weakening (compared to 19.2) to allow bundling of x and y'

speimfwALTAlternate proof of speimfw (longer compressed proof, but fewer essential steps)

spimfwSpecialization, with additional weakening (compared to sp) to allow bundling of x and y'

ax12iInference that has ax-12 (without A

Axiom scheme ax-6 (Existence)

ax6vAxiom B7 of Tarski p. 75, which requires that x and y' be distinct

ax6evAt least one individual exists

spimewExistential introduction, using implicit substitution

speivInference from existential specialization

speivwVersion of spei with a disjoint variable condition, which does not require ax-13 (neither ax-7 nor ax-12 )

exgenRule of existential generalization, similar to universal generalization ax-gen, but valid only if an individual exists

extruThere exists a variable such that wtru holds; that is, there exists a variable

19.2Theorem 19.2 of Margaris p. 89

19.2dDeduction associated with 19.2

19.8wWeak version of 19.8a and instance of 19.2d

spnfwWeak version of sp

spfalwVersion of sp when ph is false

spvwVersion of sp when x does not occur in ph

19.3vVersion of 19.3 with a disjoint variable condition, requiring fewer axioms

19.8vVersion of 19.8a with a disjoint variable condition, requiring fewer axioms

19.9vVersion of 19.9 with a disjoint variable condition, requiring fewer axioms

spimevwExistential introduction, using implicit substitution

spimvwA weak form of specialization

spsvGeneralization of antecedent

spvvSpecialization, using implicit substitution

chvarvvImplicit substitution of y' for x into a theorem

19.39Theorem 19.39 of Margaris p. 90

19.24Theorem 19.24 of Margaris p. 90

19.34Theorem 19.34 of Margaris p. 90

19.36vVersion of 19.36 with a disjoint variable condition instead of a nonfreeness hypothesis

19.12vvvVersion of 19.12vv with a disjoint variable condition, requiring fewer axioms

19.27vVersion of 19.27 with a disjoint variable condition, requiring fewer axioms

19.28vVersion of 19.28 with a disjoint variable condition, requiring fewer axioms

19.37vVersion of 19.37 with a disjoint variable condition, requiring fewer axioms

19.44vVersion of 19.44 with a disjoint variable condition, requiring fewer axioms

19.45vVersion of 19.45 with a disjoint variable condition, requiring fewer axioms

equs4vVersion of equs4 with a disjoint variable condition, which requires fewer axioms

alequexvVersion of equs4v with its consequence simplified by exsimpr

exsbimOne direction of the equivalence in exsb is based on fewer axioms

equsvIf a formula does not contain a variable x, then it is equivalent to the corresponding prototype of substitution with a fresh variable (see sb6 )

equsalvwVersion of equsalv with a disjoint variable condition, and of equsal with two disjoint variable conditions, which requires fewer axioms

equsexvwVersion of equsexv with a disjoint variable condition, and of equsex with two disjoint variable conditions, which requires fewer axioms

cbvaliwChange bound variable

cbvalivwChange bound variable

Axiom scheme ax-7 (Equality)

ax7vWeakened version of ax-7, with a disjoint variable condition on x , y

ax7v1First of two weakened versions of ax7v, with an extra disjoint variable condition on x , z, see comments there

ax7v2Second of two weakened versions of ax7v, with an extra disjoint variable condition on y , z, see comments there

equidIdentity law for equality

nfequidBound-variable hypothesis builder for x' = x'

equcomivWeaker form of equcomi with a disjoint variable condition on x , y

ax6evrA commuted form of ax6ev

ax7Proof of ax-7 from ax7v1 and ax7v2 (and earlier axioms), proving sufficiency of the conjunction of the latter two weakened versions of ax7v, which is itself a weakened version of ax-7

equcomiCommutative law for equality

equcomCommutative law for equality

equcomdDeduction form of equcom, symmetry of equality

equcomsAn inference commuting equality in antecedent

equtrA transitive law for equality

equtrrA transitive law for equality

equeuclrCommuted version of equeucl (equality is left-Euclidean)

equeuclEquality is a left-Euclidean binary relation

equequ1An equivalence law for equality

equequ2An equivalence law for equality

equtr2Equality is a left-Euclidean binary relation

stdpc6One of the two equality axioms of standard predicate calculus, called reflexivity of equality

equvinvA variable introduction law for equality

equvinvaA modified version of the forward implication of equvinv adapted to common usage

equvelvA biconditional form of equvel with disjoint variable conditions and proved from Tarski's FOL axiom schemes

ax13bAn equivalence between two ways of expressing ax-13

spfwWeak version of sp

spwWeak version of the specialization scheme sp

cbvalwChange bound variable

cbvalvwChange bound variable

cbvexvwChange bound variable

cbvaldvawRule used to change the bound variable in a universal quantifier with implicit substitution

cbvexdvawRule used to change the bound variable in an existential quantifier with implicit substitution

cbval2vwRule used to change bound variables, using implicit substitution

cbvex2vwRule used to change bound variables, using implicit substitution

cbvex4vwRule used to change bound variables, using implicit substitution

alcomimwWeak version of ax-11

excomimwWeak version of excomim

alcomwWeak version of alcom and biconditional form of alcomimw

excomwWeak version of excom and biconditional form of excomimw

hbn1fwWeak version of ax-10 from which we can prove any ax-10 instance not involving wff variables or bundling

hbn1wWeak version of hbn1

hba1wWeak version of hba1

hbe1wWeak version of hbe1

hbalwWeak version of hbal

19.8awIf a formula is true, then it is true for at least one instance

exexwExistential quantification over a given variable is idempotent

spaevA special instance of sp applied to an equality with a disjoint variable condition

cbvaevChange bound variable in an equality with a disjoint variable condition

aevlem0Lemma for aevlem

aevlemLemma for aev and axc16g

aeveqThe antecedent A

aevA "distinctor elimination" lemma with no disjoint variable conditions on variables in the consequent

aev2A version of aev with two universal quantifiers in the consequent

hbaevAll variables are effectively bound in an identical variable specifier

naevIf some set variables can assume different values, then any two distinct set variables cannot always be the same

naev2Generalization of hbnaev

hbnaevAny variable is free in -

Define proper substitution

sbjustJustification theorem for df-sb proved from Tarski's FOL axiom schemes

dfsbSimplify definition df-sb by removing its provable hypothesis

sbtlemIn the case of sbt, the hypothesis in df-sb is derivable from propositional axioms and ax-gen alone

sbtA substitution into a theorem yields a theorem

sbtruThe result of substituting in the truth constant "true" is true

stdpc4The specialization axiom of standard predicate calculus

sbtALTAlternate proof of sbt, shorter but using additional axioms

2stdpc4A double specialization using explicit substitution

sbi1Distribute substitution over implication

spsbimDistribute substitution over implication

spsbbiBiconditional property for substitution

sbimiDistribute substitution over implication

sb2imiDistribute substitution over implication

sbbiiInfer substitution into both sides of a logical equivalence

2sbbiiInfer double substitution into both sides of a logical equivalence

sbimdvDeduction substituting both sides of an implication, with ph and x disjoint

sbbidvDeduction substituting both sides of a biconditional, with ph and x disjoint

sbanConjunction inside and outside of a substitution are equivalent

sb3anThreefold conjunction inside and outside of a substitution are equivalent

spsbeExistential generalization: if a proposition is true for a specific instance, then there exists an instance where it is true

sbequEquality property for substitution, from Tarski's system

sbequiOLDObsolete version of sbequ as of 10-Aug-2026, as per conventions, paragraph "Biconditional"

sb6Alternate definition of substitution when variables are disjoint

2sb6Equivalence for double substitution

sb1vOne direction of sb5, provable from fewer axioms

sbvSubstitution for a variable not occurring in a proposition

sbcom4Commutativity law for substitution

pm11.07Axiom *11.07 in WhiteheadRussell p. 159

sbrimvwSubstitution in an implication with a variable not free in the antecedent affects only the consequent

sbrimvwOLDObsolete version of sbrimvw as of 5-Jun-2026

sbbiievAn equivalence of substitutions (as in sbbii) allowing the additional information that x = t'

sbievwConversion of implicit substitution to explicit substitution

sbiedvwConversion of implicit substitution to explicit substitution (deduction version of sbievw )

2sbievwConversion of double implicit substitution to explicit substitution

sbcom3vvSubstituting y for x and then z' for y is equivalent to substituting z' for both x and y

sbievw2sbievw applied twice, avoiding a DV condition on x, y'

sbco2vvA composition law for substitution

cbvsbvChange the bound variable (i.e

sbco4lemLemma for sbco4

sbco4Two ways of exchanging two variables

equsb3Substitution in an equality

equsb3rSubstitution applied to the atomic wff with equality

equsb1vSubstitution applied to an atomic wff

nsbAny substitution in an always false formula is false

sbn1One direction of sbn, using fewer axioms

Axiom scheme ax-8 (Left Equality for Binary Predicate)

ax8vWeakened version of ax-8, with a disjoint variable condition on x , y

ax8v1First of two weakened versions of ax8v, with an extra disjoint variable condition on x , z, see comments there

ax8v2Second of two weakened versions of ax8v, with an extra disjoint variable condition on y , z see comments there

ax8Proof of ax-8 from ax8v1 and ax8v2, proving sufficiency of the conjunction of the latter two weakened versions of ax8v, which is itself a weakened version of ax-8

elequ1An identity law for the non-logical predicate

elsb1Substitution for the first argument of the non-logical predicate in an atomic formula

cleljustWhen the class variables in Definition df-clel are replaced with setvar variables, this theorem of predicate calculus is the result

Axiom scheme ax-9 (Right Equality for Binary Predicate)

ax9vWeakened version of ax-9, with a disjoint variable condition on x , y

ax9v1First of two weakened versions of ax9v, with an extra disjoint variable condition on x , z, see comments there

ax9v2Second of two weakened versions of ax9v, with an extra disjoint variable condition on y , z see comments there

ax9Proof of ax-9 from ax9v1 and ax9v2, proving sufficiency of the conjunction of the latter two weakened versions of ax9v, which is itself a weakened version of ax-9

elequ2An identity law for the non-logical predicate

elequ2gA form of elequ2 with a universal quantifier

elsb2Substitution for the second argument of the non-logical predicate in an atomic formula

elequ12An identity law for the non-logical predicate, which combines elequ1 and elequ2

ru0The FOL statement used in the standard proof of Russell's paradox ru

Logical redundancy of ax-10 , ax-11 , ax-12 , ax-13

ax6dgenTarski's system uses the weaker ax6v instead of the bundled ax-6, so here we show that the degenerate case of ax-6 can be derived

ax10wWeak version of ax-10 from which we can prove any ax-10 instance not involving wff variables or bundling

ax11wWeak version of ax-11 from which we can prove any ax-11 instance not involving wff variables or bundling

ax11dgenDegenerate instance of ax-11 where bundled variables x and y have a common substitution

ax12wlemLemma for weak version of ax-12

ax12wWeak version of ax-12 from which we can prove any ax-12 instance not involving wff variables or bundling

ax12dgenDegenerate instance of ax-12 where bundled variables x and y have a common substitution

ax12wdemoExample of an application of ax12w that results in an instance of ax-12 for a contrived formula with mixed free and bound variables, w3a ( x e

ax13wWeak version (principal instance) of ax-13

ax13dgen1Degenerate instance of ax-13 where bundled variables x and y have a common substitution

ax13dgen2Degenerate instance of ax-13 where bundled variables x and z have a common substitution

ax13dgen3Degenerate instance of ax-13 where bundled variables y' and z have a common substitution

ax13dgen4Degenerate instance of ax-13 where bundled variables x, y, and z have a common substitution

Predicate calculus with equality: Auxiliary axiom schemes (4 schemes)

Axiom scheme ax-10 (Quantified Negation)

hbn1Alias for ax-10 to be used instead of it

hbe1The setvar x is not free in E

hbe1aDual statement of hbe1

nf5diSince the converse holds by a1i, this inference shows that we can represent a not-free hypothesis with either wnf ( \ x ph ) (inference form) or ph -> wnf ( \ x ph ) (deduction form)

nf5-1One direction of nf5 can be proved with a smaller footprint on axiom usage

nf5iDeduce that x is not free in ph from the definition

nf5dhDeduce that x is not free in ps in a context

nf5dvApply the definition of not-free in a context

nfnaewAll variables are effectively bound in a distinct variable specifier

nfe1The setvar x is not free in E

nfa1The setvar x is not free in A

nfna1A convenience theorem particularly designed to remove dependencies on ax-11 in conjunction with distinctors

nfia1Lemma 23 of Monk2 p. 114

nfnf1The setvar x is not free in wnf ( \ x ph )

modal5The analogue in our predicate calculus of axiom (5) of modal logic S5

nfs1vThe setvar x is not free in wsb y' ( \ x ph ) when x and y' are distinct

Axiom scheme ax-11 (Quantifier Commutation)

alcomsSwap quantifiers in an antecedent

alcomTheorem 19.5 of Margaris p. 89

alrot3Theorem *11.21 in WhiteheadRussell p. 160

alrot4Rotate four universal quantifiers twice

excomTheorem 19.11 of Margaris p. 89

excomimOne direction of Theorem 19.11 of Margaris p. 89

excom13Swap 1st and 3rd existential quantifiers

exrot3Rotate existential quantifiers

exrot4Rotate existential quantifiers twice

hbalIf x is not free in ph, it is not free in A

hbaldDeduction form of bound-variable hypothesis builder hbal

sbalMove universal quantifier in and out of substitution

sbalvQuantify with new variable inside substitution

hbsbwIf z is not free in ph, it is not free in wsb y' ( \ x ph ) when y' and z are distinct

sbcom2Commutativity law for substitution

nfa2Lemma 24 of Monk2 p. 114

nfexheVersion of nfex with the existential dual to the 'h' hypothesis, avoiding ax-12

nfexa2An inner universal quantifier's variable is bound

Axiom scheme ax-12 (Substitution)

ax12vThis is essentially Axiom ax-12 weakened by additional restrictions on variables

ax12v2It is possible to remove any restriction on ph in ax12v

ax12ev2Version of ax12v2 rewritten to use an existential quantifier

ax12ev2cA commuted form of ax12ev2

19.8aIf a wff is true, it is true for at least one instance

19.8adIf a wff is true, it is true for at least one instance

spiInference rule of universal instantiation, or universal specialization

spsGeneralization of antecedent

2spA double specialization (see sp )

spsdDeduction generalizing antecedent

19.2gTheorem 19.2 of Margaris p. 89, generalized to use two setvar variables

19.21biInference form of 19.21 and also deduction form of sp

19.21bbiInference removing two universal quantifiers

19.23biInference form of Theorem 19.23 of Margaris p. 90, see 19.23

nexrInference associated with the contrapositive of 19.8a

qexmidQuantified excluded middle (see exmid )

nf5rConsequence of the definition of not-free

nf5riConsequence of the definition of not-free

nf5rdConsequence of the definition of not-free in a context

spimedvDeduction version of spimev

spimefvVersion of spime with a disjoint variable condition, which does not require ax-13

nfim1A closed form of nfim

nfan1A closed form of nfan

19.3tClosed form of 19.3 and version of 19.9t with a universal quantifier

19.3A wff may be quantified with a variable not free in it

19.9dA deduction version of one direction of 19.9

19.9tClosed form of 19.9 and version of 19.3t with an existential quantifier

19.9A wff may be existentially quantified with a variable not free in it

19.21tClosed form of Theorem 19.21 of Margaris p. 90, see 19.21

19.21Theorem 19.21 of Margaris p. 90

stdpc5An axiom scheme of standard predicate calculus that emulates Axiom 5 of Mendelson p. 69

19.21-2Version of 19.21 with two quantifiers

19.23tClosed form of Theorem 19.23 of Margaris p. 90

19.23Theorem 19.23 of Margaris p. 90

alimdDeduction form of Theorem 19.20 of Margaris p. 90, see alim

alrimiInference form of Theorem 19.21 of Margaris p. 90, see 19.21

alrimddDeduction form of Theorem 19.21 of Margaris p. 90, see 19.21

alrimdDeduction form of Theorem 19.21 of Margaris p. 90, see 19.21

eximdDeduction form of Theorem 19.22 of Margaris p. 90, see exim

exlimiInference associated with 19.23

exlimdDeduction form of Theorem 19.9 of Margaris p. 89

exlimimddExistential elimination rule of natural deduction

exlimddExistential elimination rule of natural deduction

nexdDeduction for generalization rule for negated wff

albidFormula-building rule for universal quantifier (deduction form)

exbidFormula-building rule for existential quantifier (deduction form)

nfbidfAn equality theorem for effectively not free

19.16Theorem 19.16 of Margaris p. 90

19.17Theorem 19.17 of Margaris p. 90

19.27Theorem 19.27 of Margaris p. 90

19.28Theorem 19.28 of Margaris p. 90

19.19Theorem 19.19 of Margaris p. 90

19.36Theorem 19.36 of Margaris p. 90

19.36iInference associated with 19.36

19.37Theorem 19.37 of Margaris p. 90

19.32Theorem 19.32 of Margaris p. 90

19.31Theorem 19.31 of Margaris p. 90

19.41Theorem 19.41 of Margaris p. 90

19.42Theorem 19.42 of Margaris p. 90

19.44Theorem 19.44 of Margaris p. 90

19.45Theorem 19.45 of Margaris p. 90

spimfvSpecialization, using implicit substitution

chvarfvImplicit substitution of y' for x into a theorem

cbv3v2Version of cbv3 with two disjoint variable conditions, which does not require ax-11 nor ax-13

sbalexEquivalence of two ways to express proper substitution of a setvar for another setvar disjoint from it in a formula

sb4avVersion of sb4a with a disjoint variable condition, which does not require ax-13

sbimdDeduction substituting both sides of an implication

sbbidDeduction substituting both sides of a biconditional

2sbbidDeduction doubly substituting both sides of a biconditional

sbequ1An equality theorem for substitution

sbequ2An equality theorem for substitution

stdpc7One of the two equality axioms of standard predicate calculus, called substitutivity of equality

sbequ12An equality theorem for substitution

sbequ12rAn equality theorem for substitution

sbelxElimination of substitution

sbequ12aAn equality theorem for substitution

sbidAn identity theorem for substitution

sbcovA composition law for substitution

sb6aEquivalence for substitution

sbid2vwReverting substitution yields the original expression

axc16gGeneralization of axc16

axc16Proof of older axiom ax-c16

axc16gbBiconditional strengthening of axc16g

axc16nfIf dtru is false, then there is only one element in the universe, so everything satisfies F/

axc11vVersion of axc11 with a disjoint variable condition on x and y, which is provable, on top of { ax-1 -- ax-7 }, from ax12v (contrary to axc11 which seems to require the full ax-12 and ax-13 )

axc11rvVersion of axc11r with a disjoint variable condition on x and y, which is provable, on top of { ax-1 -- ax-7 }, from ax12v (contrary to axc11 which seems to require the full ax-12 and ax-13, and to axc11r which seems to require the full ax-12 )

drsb2Formula-building lemma for use with the Distinctor Reduction Theorem

equsalvAn equivalence related to implicit substitution

equsexvAn equivalence related to implicit substitution

sbftSubstitution has no effect on a nonfree variable

sbfSubstitution for a variable not free in a wff does not affect it

sbf2Substitution has no effect on a bound variable

sbhSubstitution for a variable not free in a wff does not affect it

hbs1The setvar x is not free in wsb y' ( \ x ph ) when x and y' are distinct

nfs1fIf x is not free in ph, it is not free in wsb y' ( \ x ph )

sb5Alternate definition of substitution when variables are disjoint

equs5avA property related to substitution that replaces the distinctor from equs5 to a disjoint variable condition

2sb5Equivalence for double substitution

dfsb7An alternate definition of proper substitution df-sb

sbnNegation inside and outside of substitution are equivalent

sbexMove existential quantifier in and out of substitution

nf5Alternate definition of df-nf

nf6An alternate definition of df-nf

nf5dDeduce that x is not free in ps in a context

nf5diOLDObsolete version of nf5di as of 23-Oct-2026

19.9hA wff may be existentially quantified with a variable not free in it

19.21hTheorem 19.21 of Margaris p. 90

19.23hTheorem 19.23 of Margaris p. 90

exlimihInference associated with 19.23

exlimdhDeduction form of Theorem 19.9 of Margaris p. 89

equsalhwVersion of equsalh with a disjoint variable condition, which does not require ax-13

equsexhvAn equivalence related to implicit substitution

hba1The setvar x is not free in A

hbntClosed theorem version of bound-variable hypothesis builder hbn

hbnIf x is not free in ph, it is not free in -

hbndDeduction form of bound-variable hypothesis builder hbn

hbim1A closed form of hbim

hbimdDeduction form of bound-variable hypothesis builder hbim

hbimIf x is not free in ph and ps, it is not free in ph -> ps

hbanOLDObsolete version of hban as of 22-Oct-2026

hb3anOLDObsolete version of hb3an as of 23-Oct-2026

sbi2Introduction of implication into substitution

sbimImplication inside and outside of a substitution are equivalent

sbrimSubstitution in an implication with a variable not free in the antecedent affects only the consequent

sblimSubstitution in an implication with a variable not free in the consequent affects only the antecedent

sborDisjunction inside and outside of a substitution are equivalent

sbbiEquivalence inside and outside of a substitution are equivalent

sblbisIntroduce left biconditional inside of a substitution

sbrbisIntroduce right biconditional inside of a substitution

sbrbifIntroduce right biconditional inside of a substitution

sbnfMove nonfree predicate in and out of substitution; see sbal and sbex

sbievConversion of implicit substitution to explicit substitution

sbiedwConversion of implicit substitution to explicit substitution (deduction version of sbiev )

axc7Show that the original axiom ax-c7 can be derived from ax-10 ( hbn1 ), sp and propositional calculus

axc7eAbbreviated version of axc7 using the existential quantifier

modal-bThe analogue in our predicate calculus of the Brouwer axiom (B) of modal logic S5

19.9htA closed version of 19.9h

axc4Show that the original axiom ax-c4 can be derived from ax-4 ( alim ), ax-10 ( hbn1 ), sp and propositional calculus

axc4iInference version of axc4

nfalIf x is not free in ph, then it is not free in A

nfexIf x is not free in ph, then it is not free in E

hbexIf x is not free in ph, then it is not free in E

nfnfIf x is not free in ph, then it is not free in wnf ( \ y ph )

19.12Theorem 19.12 of Margaris p. 89

nfaldDeduction form of nfal

nfexdIf x is not free in ps, then it is not free in E

nfsbvIf z is not free in ph, then it is not free in wsb y' ( \ x ph ) when z is disjoint from both x and y'

sbco2vA composition law for substitution

aaanDistribute universal quantifiers

eeorDistribute existential quantifiers

cbv3vRule used to change bound variables, using implicit substitution

cbv1vRule used to change bound variables, using implicit substitution

cbv2wRule used to change bound variables, using implicit substitution

cbvaldwDeduction used to change bound variables, using implicit substitution

cbvexdwDeduction used to change bound variables, using implicit substitution

cbv3hvRule used to change bound variables, using implicit substitution

cbvalv1Rule used to change bound variables, using implicit substitution

cbvexv1Rule used to change bound variables, using implicit substitution

cbval2vRule used to change bound variables, using implicit substitution

cbvex2vRule used to change bound variables, using implicit substitution

dvelimhwProof of dvelimh without using ax-13 but with additional distinct variable conditions

pm11.53Theorem *11.53 in WhiteheadRussell p. 164

19.12vvSpecial case of 19.12 where its converse holds

eeanDistribute existential quantifiers

eeanvDistribute a pair of existential quantifiers over a conjunction

eeeanvDistribute three existential quantifiers over a conjunction

ee4anvDistribute two pairs of existential quantifiers over a conjunction

ee4anvOLDObsolete version of ee4anv as of 26-Oct-2025

sb8vSubstitution of variable in universal quantifier

sb8fSubstitution of variable in universal quantifier

sb8efSubstitution of variable in existential quantifier

2sb8efAn equivalent expression for double existence

sb6rfvReversed substitution

sbnf2Two ways of expressing " x is (effectively) not free in ph "

exsbAn equivalent expression for existence

2exsbAn equivalent expression for double existence

sbbibReversal of substitution

sbbibvvReversal of substitution

cbvsbvfChange the bound variable (i.e

cleljustALTAlternate proof of cleljust

cleljustALT2Alternate proof of cleljust

equs5aALTAlternate proof of equs5a

equs5eALTAlternate proof of equs5e

axc11rSame as axc11 but with reversed antecedent

dral1vFormula-building lemma for use with the Distinctor Reduction Theorem

drex1vFormula-building lemma for use with the Distinctor Reduction Theorem

drnf1vFormula-building lemma for use with the Distinctor Reduction Theorem

Axiom scheme ax-13 (Quantified Equality)

ax13vA weaker version of ax-13 with distinct variable restrictions on pairs x , z and y , z

ax13lem1A version of ax13v with one distinct variable restriction dropped

ax13Derive ax-13 from ax13v and Tarski's FOL

ax13lem2Lemma for nfeqf2

nfeqf2An equation between setvar is free of any other setvar

dveeq2Quantifier introduction when one pair of variables is distinct

nfeqf1An equation between setvar is free of any other setvar

dveeq1Quantifier introduction when one pair of variables is distinct

nfeqfA variable is effectively not free in an equality if it is not either of the involved variables

axc9Derive set.mm's original ax-c9 from the shorter ax-13

ax6eAt least one individual exists

ax6Theorem showing that ax-6 follows from the weaker version ax6v

axc10Show that the original axiom ax-c10 can be derived from ax6 and axc7 (on top of propositional calculus, ax-gen, and ax-4 )

spimtClosed theorem form of spim

spimSpecialization, using implicit substitution

spimedDeduction version of spime

spimeExistential introduction, using implicit substitution

spimvA version of spim with a distinct variable requirement instead of a bound-variable hypothesis

spimvALTAlternate proof of spimv

spimevDistinct-variable version of spime

spvSpecialization, using implicit substitution

speiInference from existential specialization, using implicit substitution

chvarImplicit substitution of y' for x into a theorem

chvarvImplicit substitution of y' for x into a theorem

cbv3Rule used to change bound variables, using implicit substitution, that does not use ax-c9

cbvalRule used to change bound variables, using implicit substitution

cbvexRule used to change bound variables, using implicit substitution

cbvalvRule used to change bound variables, using implicit substitution

cbvexvRule used to change bound variables, using implicit substitution

cbv1Rule used to change bound variables, using implicit substitution

cbv2Rule used to change bound variables, using implicit substitution

cbv3hRule used to change bound variables, using implicit substitution

cbv1hRule used to change bound variables, using implicit substitution

cbv2hRule used to change bound variables, using implicit substitution

cbvaldDeduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim

cbvexdDeduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim

cbvaldvaRule used to change the bound variable in a universal quantifier with implicit substitution

cbvexdvaRule used to change the bound variable in an existential quantifier with implicit substitution

cbval2Rule used to change bound variables, using implicit substitution

cbvex2Rule used to change bound variables, using implicit substitution

cbval2vvRule used to change bound variables, using implicit substitution

cbvex2vvRule used to change bound variables, using implicit substitution

cbvex4vRule used to change bound variables, using implicit substitution

equs4Lemma used in proofs of implicit substitution properties

equsalAn equivalence related to implicit substitution

equsexAn equivalence related to implicit substitution

equsexALTAlternate proof of equsex

equsalhAn equivalence related to implicit substitution

equsexhAn equivalence related to implicit substitution

axc15Derivation of set.mm's original ax-c15 from ax-c11n and the shorter ax-12 that has replaced it

ax12Rederivation of Axiom ax-12 from ax12v (used only via sp ), axc11r, and axc15 (on top of Tarski's FOL)

ax12bA bidirectional version of axc15

ax13ALTAlternate proof of ax13 from FOL, sp, and axc9

axc11nDerive set.mm's original ax-c11n from others

aecomCommutation law for identical variable specifiers

aecomsA commutation rule for identical variable specifiers

naecomsA commutation rule for distinct variable specifiers

axc11Show that ax-c11 can be derived from ax-c11n in the form of axc11n

hbaeAll variables are effectively bound in an identical variable specifier

hbnaeAll variables are effectively bound in a distinct variable specifier

nfaeAll variables are effectively bound in an identical variable specifier

nfnaeAll variables are effectively bound in a distinct variable specifier

hbnaesRule that applies hbnae to antecedent

axc16iInference with axc16 as its conclusion

axc16nfALTAlternate proof of axc16nf, shorter but requiring ax-11 and ax-13

dral2Formula-building lemma for use with the Distinctor Reduction Theorem

dral1Formula-building lemma for use with the Distinctor Reduction Theorem

dral1ALTAlternate proof of dral1, shorter but requiring ax-11

drex1Formula-building lemma for use with the Distinctor Reduction Theorem

drex2Formula-building lemma for use with the Distinctor Reduction Theorem

drnf1Formula-building lemma for use with the Distinctor Reduction Theorem

drnf2Formula-building lemma for use with the Distinctor Reduction Theorem

nfald2Variation on nfald which adds the hypothesis that x and y are distinct in the inner subproof

nfexd2Variation on nfexd which adds the hypothesis that x and y are distinct in the inner subproof

exdistrfDistribution of existential quantifiers, with a bound-variable hypothesis saying that y is not free in ph, but x can be free in ph (and there is no distinct variable condition on x and y )

dvelimfVersion of dvelimv without any variable restrictions

dvelimdfDeduction form of dvelimf

dvelimhVersion of dvelim without any variable restrictions

dvelimThis theorem can be used to eliminate a distinct variable restriction on x and z and replace it with the "distinctor" -

dvelimvSimilar to dvelim with first hypothesis replaced by a distinct variable condition

dvelimnfVersion of dvelim using "not free" notation

dveeq2ALTAlternate proof of dveeq2, shorter but requiring ax-11

equviniA variable introduction law for equality

equvelA variable elimination law for equality with no distinct variable requirements

equs5aA property related to substitution that unlike equs5 does not require a distinctor antecedent

equs5eA property related to substitution that unlike equs5 does not require a distinctor antecedent

equs45fTwo ways of expressing substitution when y is not free in ph

equs5Lemma used in proofs of substitution properties

dveel1Quantifier introduction when one pair of variables is disjoint

dveel2Quantifier introduction when one pair of variables is disjoint

axc14Axiom ax-c14 is redundant if we assume ax-5

sb6xEquivalence involving substitution for a variable not free

sbequ5Substitution does not change an identical variable specifier

sbequ6Substitution does not change a distinctor

sb5rfReversed substitution

sb6rfReversed substitution

ax12vALTAlternate proof of ax12v2, shorter, but depending on more axioms

2ax6elemWe can always find values matching x and y, as long as they are represented by distinct variables

2ax6eWe can always find values matching x and y, as long as they are represented by distinct variables

2sb5rfReversed double substitution

2sb6rfReversed double substitution

sbel2xElimination of double substitution

sb4bSimplified definition of substitution when variables are distinct

sb3bSimplified definition of substitution when variables are distinct

sb3One direction of a simplified definition of substitution when variables are distinct

sb1One direction of a simplified definition of substitution

sb2One direction of a simplified definition of substitution

sb4aA version of one implication of sb4b that does not require a distinctor antecedent

dfsb1Alternate definition of substitution

hbsb2Bound-variable hypothesis builder for substitution

nfsb2Bound-variable hypothesis builder for substitution

hbsb2aSpecial case of a bound-variable hypothesis builder for substitution

sb4eOne direction of a simplified definition of substitution that unlike sb4b does not require a distinctor antecedent

hbsb2eSpecial case of a bound-variable hypothesis builder for substitution

hbsb3If y is not free in ph, x is not free in wsb y ( \ x ph )

nfs1If y is not free in ph, x is not free in wsb y ( \ x ph )

axc16ALTAlternate proof of axc16, shorter but requiring ax-10, ax-11, ax-13 and using df-nf and df-sb

axc16gALTAlternate proof of axc16g that uses df-sb and requires ax-10, ax-11, ax-13

equsb1Substitution applied to an atomic wff

equsb2Substitution applied to an atomic wff

dfsb2An alternate definition of proper substitution that, like dfsb1, mixes free and bound variables to avoid distinct variable requirements

dfsb3An alternate definition of proper substitution df-sb that uses only primitive connectives (no defined terms) on the right-hand side

drsb1Formula-building lemma for use with the Distinctor Reduction Theorem

sb2aeIn the case of two successive substitutions for two always equal variables, the second substitution has no effect

sb6fEquivalence for substitution when y is not free in ph

sb5fEquivalence for substitution when y is not free in ph

nfsb4tA variable not free in a proposition remains so after substitution in that proposition with a distinct variable (closed form of nfsb4 )

nfsb4A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (inference associated with nfsb4t )

sbequ8Elimination of equality from antecedent after substitution

sbieConversion of implicit substitution to explicit substitution

sbiedConversion of implicit substitution to explicit substitution (deduction version of sbie) Usage of this theorem is discouraged because it depends on ax-13

sbiedvConversion of implicit substitution to explicit substitution (deduction version of sbie )

2sbievConversion of double implicit substitution to explicit substitution

sbcom3Substituting y for x and then z' for y is equivalent to substituting z' for both x and y

sbcoA composition law for substitution

sbid2An identity law for substitution

sbid2vAn identity law for substitution

sbidmAn idempotent law for substitution

sbco2A composition law for substitution

sbco2dA composition law for substitution

sbco3A composition law for substitution

sbcomA commutativity law for substitution

sbtrtPartially closed form of sbtr

sbtrA partial converse to sbt

sb8Substitution of variable in universal quantifier

sb8eSubstitution of variable in existential quantifier

sb9Commutation of quantification and substitution variables

sb9iCommutation of quantification and substitution variables

sbhbTwo ways of expressing " x is (effectively) not free in ph "

nfsbdDeduction version of nfsb

nfsbIf z is not free in ph, then it is not free in wsb y' ( \ x ph ) when y' and z are distinct

hbsbIf z is not free in ph, then it is not free in wsb y' ( \ x ph ) when y' and z are distinct

sb7fThis version of dfsb7 does not require that ph and z be disjoint

sb7hThis version of dfsb7 does not require that ph and z be disjoint

sb10fHao Wang's identity axiom P6 in Irving Copi, Symbolic Logic (5th ed., 1979), p. 328

sbal1Check out sbal for a version not dependent on ax-13

sbal2Move quantifier in and out of substitution

2sb8eAn equivalent expression for double existence

Uniqueness and unique existence

dfmoeuAn elementary proof of moeu in disguise, connecting an expression characterizing uniqueness ( df-mo) to that of existential uniqueness ( eu6 )

dfeumoAn elementary proof showing the reverse direction of dfmoeu

Uniqueness: the at-most-one quantifier

mojustSoundness justification theorem for df-mo

dfmoSimplify definition df-mo by removing its provable hypothesis

nexmoNonexistence implies uniqueness

exmoAny proposition holds for some x or holds for at most one x

moabsAbsorption of existence condition by uniqueness

moimThe at-most-one quantifier reverses implication

moimiThe at-most-one quantifier reverses implication

moimdvThe at-most-one quantifier reverses implication, deduction form

mobiEquivalence theorem for the at-most-one quantifier

mobiiFormula-building rule for the at-most-one quantifier (inference form)

mobidvFormula-building rule for the at-most-one quantifier (deduction form)

mobidFormula-building rule for the at-most-one quantifier (deduction form)

moa1If an implication holds for at most one value, then its consequent holds for at most one value

moan"At most one" is still the case when a conjunct is added

moani"At most one" is still true when a conjunct is added, inference form

moor"At most one" is still the case when a disjunct is removed

mooran1"At most one" imports disjunction to conjunction

mooran2"At most one" exports disjunction to conjunction

nfmo1Bound-variable hypothesis builder for the at-most-one quantifier

nfmod2Bound-variable hypothesis builder for the at-most-one quantifier

nfmodvBound-variable hypothesis builder for the at-most-one quantifier

nfmovBound-variable hypothesis builder for the at-most-one quantifier

nfmodBound-variable hypothesis builder for the at-most-one quantifier

nfmoBound-variable hypothesis builder for the at-most-one quantifier

mofVersion of df-mo with disjoint variable condition replaced by nonfreeness hypothesis

mo3Alternate definition of the at-most-one quantifier

moEquivalent definitions of "there exists at most one"

mo4At-most-one quantifier expressed using implicit substitution

mo4fAt-most-one quantifier expressed using implicit substitution

Unique existence: the unique existential quantifier

eu3vAn alternate way to express existential uniqueness

eujustSoundness justification theorem for eu6 when this was the definition of the unique existential quantifier (note that y and z need not be disjoint, although the weaker theorem with that disjoint variable condition added would be enough to justify the soundness of the definition)

eujustALTAlternate proof of eujust illustrating the use of dvelim

eu6lemLemma of eu6im

eu6Alternate definition of the unique existential quantifier df-eu not using the at-most-one quantifier

eu6imOne direction of eu6 needs fewer axioms

eufVersion of eu6 with disjoint variable condition replaced by nonfreeness hypothesis

euexExistential uniqueness implies existence

eumoExistential uniqueness implies uniqueness

eumoiUniqueness inferred from existential uniqueness

exmoeubExistence implies that uniqueness is equivalent to unique existence

exmoeuExistence is equivalent to uniqueness implying existential uniqueness

moeuexUniqueness implies that existence is equivalent to unique existence

moeuUniqueness is equivalent to existence implying unique existence

eubiEquivalence theorem for the unique existential quantifier

eubiiIntroduce unique existential quantifier to both sides of an equivalence

eubidvFormula-building rule for unique existential quantifier (deduction form)

eubidFormula-building rule for the unique existential quantifier (deduction form)

nfeu1ALTAlternate version of nfeu1 with a shorter proof but using ax-12

nfeu1Bound-variable hypothesis builder for uniqueness

nfeud2Bound-variable hypothesis builder for uniqueness

nfeudwBound-variable hypothesis builder for the unique existential quantifier

nfeudBound-variable hypothesis builder for the unique existential quantifier

nfeuwBound-variable hypothesis builder for the unique existential quantifier

nfeuBound-variable hypothesis builder for the unique existential quantifier

dfeuRederive df-eu from the old definition eu6

dfmo2Rederive df-mo from the old definition moeu

euequThere exists a unique set equal to a given set

sb8euvVariable substitution in unique existential quantifier

sb8euVariable substitution in unique existential quantifier

sb8moVariable substitution for the at-most-one quantifier

cbvmovwChange bound variable

cbvmowRule used to change bound variables, using implicit substitution

cbvmoRule used to change bound variables, using implicit substitution

cbveuvwChange bound variable

cbveuwVersion of cbveu with a disjoint variable condition, which does not require ax-10, ax-13

cbveuRule used to change bound variables, using implicit substitution

cbveuALTAlternative proof of cbveu

eu2An alternate way of defining existential uniqueness

eu1An alternate way to express uniqueness used by some authors

euorIntroduce a disjunct into a unique existential quantifier

euorvIntroduce a disjunct into a unique existential quantifier

euor2Introduce or eliminate a disjunct in a unique existential quantifier

sbmoSubstitution into an at-most-one quantifier

eu4Uniqueness using implicit substitution

euimmoExistential uniqueness implies uniqueness through reverse implication

euimAdd unique existential quantifiers to an implication

moanimlemFactor out the common proof skeleton of moanimv and moanim

moanimvIntroduction of a conjunct into an at-most-one quantifier

moanimIntroduction of a conjunct into "at most one" quantifier

euanIntroduction of a conjunct into unique existential quantifier

moanmoNested at-most-one quantifiers

moaneuNested at-most-one and unique existential quantifiers

euanvIntroduction of a conjunct into unique existential quantifier

mopick"At most one" picks a variable value, eliminating an existential quantifier

moexexlemFactor out the proof skeleton of moexex and moexexvw

2moexvDouble quantification with "at most one"

moexexvw"At most one" double quantification

2moswapvA condition allowing to swap an existential quantifier and at at-most-one quantifier

2euswapvA condition allowing to swap an existential quantifier and a unique existential quantifier

2euexvDouble quantification with existential uniqueness

2exeuvDouble existential uniqueness implies double unique existential quantification

eupickExistential uniqueness "picks" a variable value for which another wff is true

eupickaVersion of eupick with closed formulas

eupickbExistential uniqueness "pick" showing wff equivalence

eupickbiTheorem *14.26 in WhiteheadRussell p. 192

mopick2"At most one" can show the existence of a common value

moexex"At most one" double quantification

moexexv"At most one" double quantification

2moexDouble quantification with "at most one"

2euexDouble quantification with existential uniqueness

2eumoNested unique existential quantifier and at-most-one quantifier

2eu2exDouble existential uniqueness

2moswapA condition allowing to swap an existential quantifier and at at-most-one quantifier

2euswapA condition allowing to swap an existential quantifier and a unique existential quantifier

2exeuDouble existential uniqueness implies double unique existential quantification

2mo2Two ways of expressing "there exists at most one ordered pair <

2moTwo ways of expressing "there exists at most one ordered pair <

2mosDouble "there exists at most one", using implicit substitution

2eu1Double existential uniqueness

2eu1vDouble existential uniqueness

2eu2Double existential uniqueness

2eu3Double existential uniqueness

2eu4This theorem provides us with a definition of double existential uniqueness ("exactly one x and exactly one y ")

2eu5An alternate definition of double existential uniqueness (see 2eu4 )

2eu6Two equivalent expressions for double existential uniqueness

2eu7Two equivalent expressions for double existential uniqueness

2eu8Two equivalent expressions for double existential uniqueness

euaeTwo ways to express "exactly one thing exists"

exists1Two ways to express "exactly one thing exists"

exists2A condition implying that at least two things exist

Other axiomatizations related to classical predicate calculus

Aristotelian logic: Assertic syllogisms

barbara"Barbara", one of the fundamental syllogisms of Aristotelian logic

celarent"Celarent", one of the syllogisms of Aristotelian logic

darii"Darii", one of the syllogisms of Aristotelian logic

dariiALTAlternate proof of darii, shorter but using more axioms

ferio"Ferio" ("Ferioque"), one of the syllogisms of Aristotelian logic

barbarilemLemma for barbari and the other Aristotelian syllogisms with existential assumption

barbari"Barbari", one of the syllogisms of Aristotelian logic

barbariALTAlternate proof of barbari, shorter but using more axioms

celaront"Celaront", one of the syllogisms of Aristotelian logic

cesare"Cesare", one of the syllogisms of Aristotelian logic

camestres"Camestres", one of the syllogisms of Aristotelian logic

festino"Festino", one of the syllogisms of Aristotelian logic

festinoALTAlternate proof of festino, shorter but using more axioms

baroco"Baroco", one of the syllogisms of Aristotelian logic

barocoALTAlternate proof of festino, shorter but using more axioms

cesaro"Cesaro", one of the syllogisms of Aristotelian logic

camestros"Camestros", one of the syllogisms of Aristotelian logic

datisi"Datisi", one of the syllogisms of Aristotelian logic

disamis"Disamis", one of the syllogisms of Aristotelian logic

ferison"Ferison", one of the syllogisms of Aristotelian logic

bocardo"Bocardo", one of the syllogisms of Aristotelian logic

darapti"Darapti", one of the syllogisms of Aristotelian logic

daraptiALTAlternate proof of darapti, shorter but using more axioms

felapton"Felapton", one of the syllogisms of Aristotelian logic

calemes"Calemes", one of the syllogisms of Aristotelian logic

dimatis"Dimatis", one of the syllogisms of Aristotelian logic

fresison"Fresison", one of the syllogisms of Aristotelian logic

calemos"Calemos", one of the syllogisms of Aristotelian logic

fesapo"Fesapo", one of the syllogisms of Aristotelian logic

bamalip"Bamalip", one of the syllogisms of Aristotelian logic

Intuitionistic logic

axia1Left 'and' elimination (intuitionistic logic axiom ax-ia1)

axia2Right 'and' elimination (intuitionistic logic axiom ax-ia2)

axia3'And' introduction (intuitionistic logic axiom ax-ia3)

axin1'Not' introduction (intuitionistic logic axiom ax-in1)

axin2'Not' elimination (intuitionistic logic axiom ax-in2)

axioDefinition of 'or' (intuitionistic logic axiom ax-io)

axi4Specialization (intuitionistic logic axiom ax-4)

axi5rConverse of axc4 (intuitionistic logic axiom ax-i5r)

axialThe setvar x is not free in A

axie1The setvar x is not free in E

axie2A key property of existential quantification (intuitionistic logic axiom ax-ie2)

axi9Axiom of existence (intuitionistic logic axiom ax-i9)

axi10Axiom of Quantifier Substitution (intuitionistic logic axiom ax-10)

axi12Axiom of Quantifier Introduction (intuitionistic logic axiom ax-i12)

axbndAxiom of Bundling (intuitionistic logic axiom ax-bnd)