# List of theorems

List of theorems in peano_new/prop.gh:

dummylink # <context> # This theorem is part of a series of proofs about # <a href="/wiki/peano/logic"> propositional logic </a> which is concerned # with true and false statements and rules of inference. # </context>
ph , psph
a1i # <title> First Axiom Inference </title> # <table> # [ ph # (-> ps [ ph) # </table>
ph(-> ps ph)
a2i # <title> Second Axiom Inference </title> # <table> # (-> ph ] (-> [ ps ] [ ch)) # (-> (-> ph ] [ ps ] ) (-> ph [ ch)) # </table>
(-> ph (-> ps ch))(-> (-> ph ps) (-> ph ch))
syl # <title> Syllogism </title> # <table> # (-> ph [ ps ] ] ] ) # [ (-> ps ] [ ch ] ) # (-> ph [ [ [ ch ] ) # </table>
(-> ph ps) , (-> ps ch)(-> ph ch)
com12 # <title> Commute First and Second Antecedents </title> # <table> # (-> <r> ph (-> <g> ps ch)) # (-> <g> ps (-> <r> ph ch)) # </table>
(-> ph (-> ps ch))(-> ps (-> ph ch))
a1d # <title> First Axiom Deduction </title> # <table> # [ ph # (-> ps [ ph) # </table>
(-> ph ps)(-> ph (-> ch ps))
a2d # <title> Second Axiom Deduction </title> # <table> # (-> ph (-> ps ] (-> [ ch ] [ th))) # (-> ph (-> (-> ps ] [ ch ] ) (-> ps [ th))) # </table>
(-> ph (-> ps (-> ch th)))(-> ph (-> (-> ps ch) (-> ps th)))
himp1i # <table> # (-> (-> ph [ ps ] ) [ ch) # (-> [ ps ] [ ch) # </table>
(-> (-> ph ps) ch)(-> ps ch)
imim2 # <title> Syllogism (Closed Form) </title>
(-> (-> ph ps) (-> (-> ch ph) (-> ch ps)))
imim1 a.k.a. sylt # <title> Syllogism (Closed Form) </title>
(-> (-> ph ps) (-> (-> ps ch) (-> ph ch)))
imim1i # <title> Syllogism </title> # <summary> # The theorem <a href="imim1">imim1</a> written as an inference. # </summary>
(-> ph ps)(-> (-> ps ch) (-> ph ch))
imim2i # <title> Syllogism </title> # <summary> # The theorem <a href="imim2">imim2</a> written as an inference. # </summary> # <table> # (-> [ ph ] [ ps) # (-> (-> ch [ ph ] ) (-> ch [ ps)) # </table>
(-> ph ps)(-> (-> ch ph) (-> ch ps))
imim12i # <title> Inference joining two implications (Bridge) </title>
(-> ph ps) , (-> ch th)(-> (-> ps ch) (-> ph th))
imim3i # <title> Inference adding three nested antecedents. </title>
(-> ph (-> ps ch))(-> (-> th ph) (-> (-> th ps) (-> th ch)))
3syl # <title> Inference chaining two syllogisms </title>
(-> ph ps) , (-> ps ch) , (-> ch th)(-> ph th)
syl5 # <title> A syllogism rule of inference </title> # <summary> # The second premise is used to replace the second antecedent of the first premise. # </summary>
(-> ph (-> ps ch)) , (-> th ps)(-> ph (-> th ch))
syl6 # <title> A syllogism rule of inference </title> # <summary> # The second premise is used to replace the consequent of the first premise. # </summary>
(-> ph (-> ps ch)) , (-> ch th)(-> ph (-> ps th))
syl7 # <title> A syllogism rule of inference </title> # <summary> # The second premise is used to replace the third antecedent of the first premise. # </summary>
(-> ph (-> ps (-> ch th))) , (-> ta ch)(-> ph (-> ps (-> ta th)))
syl8 # <title> A syllogism rule of inference </title> # <summary> # The second premise is used to replace the consequent of the first premise. # </summary>
(-> ph (-> ps (-> ch th))) , (-> th ta)(-> ph (-> ps (-> ch ta)))
imim2d # <title> Deduction adding nested antecedents </title>
(-> ph (-> ps ch))(-> ph (-> (-> th ps) (-> th ch)))
mpd # <title> Modus Ponens </title> # <table> # (-> ph [ ps ] ] ) # (-> ph (-> [ ps ] [ ch)) # (-> ph [ [ [ ch) # </table>
(-> ph ps) , (-> ph (-> ps ch))(-> ph ch)
syld # <title> Syllogism Deduction </title> # <summary> # Notice that this has the same form as <a href="syl">syl</a> with ph added in front of each # hypothesis and conclusion. When all theorems referenced in a proof are converted in this # way, we can replace ph with a hypothesis of the proof, allowing the hypothesis to be # eliminated with <a href="id">id</a> and become an antecedent. # </summary>
(-> ph (-> ps ch)) , (-> ph (-> ch th))(-> ph (-> ps th))
imim1d # <title> Deduction adding nested consequents </title> # <summary> # The theorem <a href="imim1">imim1</a> written as an deduction. # </summary>
(-> ph (-> ps ch))(-> ph (-> (-> ch th) (-> ps th)))
imim12d # <title> Deduction combining antecedents and consequents </title>
(-> ph (-> ps ch)) , (-> ph (-> th ta))(-> ph (-> (-> ch th) (-> ps ta)))
pm2.04 aka com12t # <title> Commute First and Second Antecedents </title> # <summary> # One line version of <a href="com12">com12</a>. # </summary> # <table> # (-> (-> <r> ph (-> <g> ps ch)) (-> <g> ps (-> <r> ph ch))) # </table>
(-> (-> ph (-> ps ch)) (-> ps (-> ph ch)))
(-> (-> ph (-> ps ch)) (-> (-> ph (-> ch th)) (-> ph (-> ps th))))
com23 # <title> Commute Second and Third Antecedents </title> # <table> # (-> ph (-> <r> ps (-> <g> ch th))) # (-> ph (-> <g>ch (-> <r> ps th))) # </table>
(-> ph (-> ps (-> ch th)))(-> ph (-> ch (-> ps th)))
com13 # <title> Commute First and Third Antecedents </title>
(-> ph (-> ps (-> ch th)))(-> ch (-> ps (-> ph th)))
com3l # <title> Commute Antecedents (Rotate Left) </title>
(-> ph (-> ps (-> ch th)))(-> ps (-> ch (-> ph th)))
com3r # <title> Commute Antecedents (Rotate Right) </title>
(-> ph (-> ps (-> ch th)))(-> ch (-> ph (-> ps th)))
com34 # <title> Commute Third and Fourth Antecedents </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> ph (-> ps (-> th (-> ch ta))))
com24 # <title> Commute Second and Fourth Antecedents </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> ph (-> th (-> ch (-> ps ta))))
com14 # <title> Commute First and Fourth Antecedents </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> th (-> ps (-> ch (-> ph ta))))
com4l # <title> Commute Antecedents (Rotate Left) </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> ps (-> ch (-> th (-> ph ta))))
com4t # <title> Commute Antecedents (Rotate Twice) </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> ch (-> th (-> ph (-> ps ta))))
com4r # <title> Commute Antecedents (Rotate Right) </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> th (-> ph (-> ps (-> ch ta))))
a1dd # <title> Introducing an embedded antecedent </title>
(-> ph (-> ps ch))(-> ph (-> ps (-> th ch)))
mp2 # <title> Double Modus Ponens </title>
ph , ps , (-> ph (-> ps ch))ch
mpi # <title> Modus Ponens Inference </title>
ps , (-> ph (-> ps ch))(-> ph ch)
mpii # <title> Modus Ponens Inference </title>
ch , (-> ph (-> ps (-> ch th)))(-> ph (-> ps th))
mpdd # <title> Modus Ponens Deduction </title>
(-> ph (-> ps ch)) , (-> ph (-> ps (-> ch th)))(-> ph (-> ps th))
mpid # <title> Modus Ponens Deduction </title>
(-> ph ch) , (-> ph (-> ps (-> ch th)))(-> ph (-> ps th))
mpdi # <title> Modus Ponens Deduction </title>
(-> ps ch) , (-> ph (-> ps (-> ch th)))(-> ph (-> ps th))
mpcom # <title> Modus Ponens & Commute Antecedents </title>
(-> ps ph) , (-> ph (-> ps ch))(-> ps ch)
syldd # <title> Syllogism deduction </title>
(-> ph (-> ps (-> ch th))) , (-> ph (-> ps (-> th ta)))(-> ph (-> ps (-> ch ta)))
sylcom # <title> Syllogism & Commute Antecedents </title>
(-> ph (-> ps ch)) , (-> ps (-> ch th))(-> ph (-> ps th))
syl5com Hmm, this is the kind of thing where it's easier to just use syl5 com12 rather than introduce a new name syl5com ... There should be a proof complexity metric that reflects that. # <title> Syllogism & Commute Antecedents </title>
(-> ph (-> ps ch)) , (-> th ps)(-> th (-> ph ch))
syl6com # <title> Syllogism & Commute Antecedents </title>
(-> ph (-> ps ch)) , (-> ch th)(-> ps (-> ph th))
syli # <title> Syllogism </title> # <summary> Syllogism inference with common nested antecedent. </summary>
(-> ps (-> ph ch)) , (-> ch (-> ph th))(-> ps (-> ph th))
syl5d # <title> Syllogism Deduction </title>
(-> ph (-> ps (-> ch th))) , (-> ph (-> ta ch))(-> ph (-> ps (-> ta th)))
syl6d # <title> Syllogism Deduction </title>
(-> ph (-> ps (-> ch th))) , (-> ph (-> th ta))(-> ph (-> ps (-> ch ta)))
syl9 # <title> Syllogism Deduction </title>
(-> ph (-> ps ch)) , (-> th (-> ch ta))(-> ph (-> th (-> ps ta)))
syl9r # <title> Syllogism Deduction </title>
(-> ph (-> ps ch)) , (-> th (-> ch ta))(-> th (-> ph (-> ps ta)))
id # <title> Identity </title> # <table> # (-> <g> ph <g> ph) # </table> # <summary> # See <a href="id1">id1</a> for an alternative proof directly from the axioms. # </summary>
(-> ph ph)
id1 # <title> Identity </title> # <summary> # This version is proved directly from the axioms for demonstration purposes. # This proof is a popular example in the literature. For an alternative proof # see <a href="id">id</a>. # </summary> # <table> # (-> <g> ph <g> ph) # </table>
(-> ph ph)
idd # <title> Identity Deduction </title> # <summary> # <a href="id">Identity</a> written as an deduction. # </summary>
(-> ph (-> ps ps))
pm2.27 # <title> Modus Ponens </title> # <summary> # This theorem can be thought of as a closed form of modus ponens. # </summary>
(-> ph (-> (-> ph ps) ps))
hid # <table> # (-> (-> ph ph) [ ps) # [ ps # </table>
(-> (-> ph ph) ps)ps
pm2.43 # <title> Absorb redundant antecedent </title> # <summary> # Absorption of redundant antecedent. Also called the "Contraction" or # "Hilbert" axiom. # </summary>
(-> (-> ph (-> ph ps)) (-> ph ps))
pm2.43i a.k.a. impsimpi # <title> Absorb redundant antecedent </title> # <table> # (-> <r> ph [ (-> <r> ph ps)) # [ (-> <r> ph ps) # </table>
(-> ph (-> ph ps))(-> ph ps)
pm2.43d # <title> Absorb redundant antecedent </title> # <table> # (-> ph [ (-> <r> ps [ (-> <r> ps ch))) # (-> ph [ [ (-> <r> ps ch)) # </table>
(-> ph (-> ps (-> ps ch)))(-> ph (-> ps ch))
pm2.43a # <title> Absorb redundant antecedent </title>
(-> ps (-> ph (-> ps ch)))(-> ps (-> ph ch))
pm2.43b # <title> Absorb redundant antecedent </title>
(-> ps (-> ph (-> ps ch)))(-> ph (-> ps ch))
sylc # <title> Syllogism & Contraction </title>
(-> ph (-> ps ch)) , (-> th ph) , (-> th ps)(-> th ch)
himp1 # <table> # (-> (-> (-> <r> ph <g> ps) <b> ch) (-> <g> ps <b> ch)) # </table>
(-> (-> (-> ph ps) ch) (-> ps ch))
pm2.86 # <title> Converse of ax-2 </title>
(-> (-> (-> ph ps) (-> ph ch)) (-> ph (-> ps ch)))
pm2.86i # <title> Converse of ax-2 </title> # <summary> # <a href="pm2.86">pm2.86</a> written as an inference. # </summary>
(-> (-> ph ps) (-> ph ch))(-> ph (-> ps ch))
pm2.86d # <title> Converse of ax-2 </title> # <summary> # <a href="pm2.86">pm2.86</a> written as an deduction. # </summary>
(-> ph (-> (-> ps ch) (-> ps th)))(-> ph (-> ps (-> ch th)))
loolin # <title> Lukasiewicz's Linearity Axiom </title> # <summary> # The Linearity Axiom of the infinite-valued sentential logic (L-infinity) # of <a href="http://en.wikipedia.org/wiki/Jan_%C5%81ukasiewicz">Lukasiewicz</a>. # </summary>
(-> (-> (-> ph ps) (-> ps ph)) (-> ps ph))
loowoz # <title> Lukasiewicz's Linearity Axiom </title> # <summary> # An alternate for the Linearity Axiom of the infinite-valued sentential # logic (L-infinity) of Lukasiewicz, due to Barbara Wozniakowska. # </summary>
(-> (-> (-> ph ps) (-> ph ch)) (-> (-> ps ph) (-> ps ch)))
a3i Yeah, negation! # <title> Third Axiom Inference </title>
(-> (-. ph) (-. ps))(-> ps ph)
con4i # <title> Third Axiom Inference </title> # <summary> # Same as <a href="a3i">a3i</a> just a different name. # </summary>
(-> (-. ph) (-. ps))(-> ps ph)
con4d a.k.a. a3d # <title> Third Axiom Deduction </title>
(-> ph (-> (-. ps) (-. ch)))(-> ph (-> ch ps))
a3d # <title> Third Axiom Deduction </title> # <summary> # Same as <a href="con4d">con4d</a> just a different name. # </summary>
(-> ph (-> (-. ps) (-. ch)))(-> ph (-> ch ps))
pm2.21 a.k.a. a1n # <title> Contradiction Implies Anything </title> # <summary> # From a wff and its negation, anything is true. Also called the # <a href="http://en.wikipedia.org/wiki/Duns_Scotus">Duns Scotus</a> law. # </summary>
(-> (-. ph) (-> ph ps))
pm2.21i # <title> Contradiction Implies Anything </title> # <summary> # The theorem <a href="pm2.21">pm2.21</a> written as an inference. # </summary>
(-. ph)(-> ph ps)
pm2.21d # <title> Contradiction Implies Anything </title> # <summary> # The theorem <a href="pm2.21">pm2.21</a> written as a deduction. # </summary>
(-> ph (-. ps))(-> ph (-> ps ch))
pm2.24 # <title> Contradiction Implies Anything </title>
(-> ph (-> (-. ph) ps))
pm2.24i # <title> Contradiction Implies Anything </title> # <summary> # The theorem <a href="pm2.24">pm2.24</a> written as an inference. # </summary>
ph(-> (-. ph) ps)
pm2.24d # <title> Contradiction Implies Anything </title> # <summary> # The theorem <a href="pm2.24">pm2.24</a> written as a deduction. # </summary> # <title> Contradiction Implies Anything </title>
(-> ph ps)(-> ph (-> (-. ps) ch))
pm2.24ii # <title> Contradiction Implies Anything </title> # <summary> # The theorem <a href="pm2.24">pm2.24</a> written as an inference. # </summary>
ph , (-. ph)ps
(-> (-> ph ps) ch)(-> (-. ph) ch)
(-> (-> (-> ph ps) ch) (-> (-. ph) ch))
(-> (-> (-. (-. ph)) (-. (-. ps))) (-> ph ps))
(-> (-. (-. ph)) ph)
(-> ph (-. (-. ph)))
(-. (-. ph))ph
ph(-. (-. ph))
(-> ph (-. (-. ps)))(-> ph ps)
(-> ph ps)(-> ph (-. (-. ps)))
con1 # <title> Contraposition </title>
(-> (-> (-. ph) ps) (-> (-. ps) ph))
con2 # <title> Contraposition </title>
(-> (-> ph (-. ps)) (-> ps (-. ph)))
con3 # <title> Contraposition </title>
(-> (-> ph ps) (-> (-. ps) (-. ph)))
con1i # <title> Contraposition </title>
(-> (-. ph) ps)(-> (-. ps) ph)
con2i # <title> Contraposition </title> # <table> # (-> <r> ph (-. <g> ps)) # (-> <g> ps (-. <r> ph)) # </table>
(-> ph (-. ps))(-> ps (-. ph))
con3i # <title> Contraposition </title> # <table> # (-> <r> ph <g> ps ) # (-> <g> (-. ps) <r> (-. ph)) # </table>
(-> ph ps)(-> (-. ps) (-. ph))
con1d a.k.a. con1d # <title> Contraposition </title>
(-> ph (-> (-. ps) ch))(-> ph (-> (-. ch) ps))
con2d # <title> Contraposition </title>
(-> ph (-> ps (-. ch)))(-> ph (-> ch (-. ps)))
con3d # <title> Contraposition </title>
(-> ph (-> ps ch))(-> ph (-> (-. ch) (-. ps)))
(-> (-. (-> ph ps)) ph)
(-> (-. (-> ph ps)) (-. ps))
nimp aka mth8
(-> ph (-> (-. ps) (-. (-> ph ps))))
pm2.18 a.k.a. npipip # <title> Proof by contradiction </title> # <summary> # Also called the Law of <a href="http://en.wikipedia.org/wiki/Christopher_Clavius">Clavius</a>. # Metamath seems to have a fairly short but tricky proof of pm2.18 that # doesn't detour through dn, nimp, con1, et. al.; but we need those # anyway and pm2.18 is proven more straightforwardly once we have nimp. # </summary>
(-> (-> (-. ph) ph) ph)
pm2.18_mm # <title> Proof by contradiction </title>
(-> (-> (-. ph) ph) ph)
(-. (-> ph ps))ph
(-. (-> ph ps))(-. ps)
ph , (-. ps)(-. (-> ph ps))
(-> ph ps) , (-> ph (-. ch))(-> ph (-. (-> ps ch)))
preand1 # <title> Simplification </title> # <summary> # This is the same as <a href="pm3.26">pm3.26</a>, but uses the primitive # connectives → and ¬ instead of conjunction. This is exactly the same as # <a href="pm3.26im">pm3.26im</a> # </summary>
(-> (-. (-> ph (-. ps))) ph)
preand2 # <title> Simplification </title> # <summary> # This is the same as <a href="pm3.27">pm3.27</a>, but uses the primitive # connectives → and ¬ instead of conjunction. This is exactly the same as # <a href="pm3.27im">pm3.27im</a> # </summary>
(-> (-. (-> ph (-. ps))) ps)
preand # <title> Join antecedents </title> # <summary> # This is the same as <a href="pm3.2im">pm3.2im</a>, but uses the primitive # connectives → and ¬ instead of conjunction. This is exactly the same as # <a href="pm3.2im">pm3.2im</a> # </summary>
(-> ph (-> ps (-. (-> ph (-. ps)))))
preand1i # <title> Simplification </title>
(-. (-> ph (-. ps)))ph
preand2i # <title> Simplification </title>
(-. (-> ph (-. ps)))ps
preandi # <title> Join premises </title>
ph , ps(-. (-> ph (-. ps)))
jc # <title> Join the consequents of two premises </title>
(-> ph ps) , (-> ph ch)(-> ph (-. (-> ps (-. ch))))
df-and # <title> Definition of AND </title> # <summary> # Define conjunction, logical AND. # This theorem writes the definition of AND without using the biconditional. The # theorem <a href="df-an">df-an</a> rewrites this definition in a more familiar # form. # </summary>
(-. (-> (-> (/\ ph ps) (-. (-> ph (-. ps)))) (-. (-> (-. (-> ph (-. ps))) (/\ ph ps)))))
df-and-1 # <title> Definition of AND Implication </title>
(-> (/\ ph ps) (-. (-> ph (-. ps))))
df-and-2 # <title> Definition of AND Implication </title>
(-> (-. (-> ph (-. ps))) (/\ ph ps))
df-and-1i # <title> Definition of AND Implication </title>
(/\ ph ps)(-. (-> ph (-. ps)))
df-and-2i # <title> Definition of AND Implication </title>
(-. (-> ph (-. ps)))(/\ ph ps)
df-and-1d # <title> Definition of AND Deduction </title>
(-> ph (/\ ps ch))(-> ph (-. (-> ps (-. ch))))
df-and-2d # <title> Definition of AND Deduction </title>
(-> ph (-. (-> ps (-. ch))))(-> ph (/\ ps ch))
and1 # <title> Eliminate Conjunct </title>
(-> (/\ ph ps) ph)
and2 # <title> Eliminate Conjunct </title>
(-> (/\ ph ps) ps)
and # <title> Join consequents </title>
(-> ph (-> ps (/\ ph ps)))
and1i # <title> Eliminate Conjunct </title>
(/\ ph ps)ph
and2i # <title> Eliminate Conjunct </title>
(/\ ph ps)ps
pm3.2i # <title> Conjunction from premises </title> # <table> # ph ] ] # [ [ ps # (/\ ph ] [ ps) # </table>
ph , ps(/\ ph ps)
and1d # <title> Eliminate Conjunct </title>
(-> ph (/\ ps ch))(-> ph ps)
and2d # <title> Eliminate Conjunct </title>
(-> ph (/\ ps ch))(-> ph ch)
andd # <title> Join consequents </title>
(-> ph ps) , (-> ph ch)(-> ph (/\ ps ch))
def-bi # <title> Definition of Biconditional </title> # <summary> # This is our first definition, which introduces and defines the # biconditional connective {{{<->}}}. We define a wff of the form # #(<-> ph ps)# as an abbreviation for # #(-. (-> (-> ph ps) (-. (-> ps ph))))#. # # Unlike most traditional developments, we have chosen not to have a # separate symbol such as "Df." to mean "is defined as." Instead, we will # later use the biconditional connective for this purpose (<a href="df-or">df-or</a> is its # first use), as it allows us to use logic to manipulate definitions # directly. This greatly simplifies many proofs since it eliminates the # need for a separate mechanism for introducing and eliminating # definitions. Of course, we cannot use this mechanism to define the # biconditional itself, since it hasn't been introduced yet. Instead, we # use a more general form of definition, described as follows. # # In its most general form, a definition is simply an assertion that # introduces a new symbol that is eliminable and does not strengthen the existing # language. The latter requirement means that the set of provable # statements not containing the new symbol (or new combination) should # remain exactly the same after the definition is introduced. Our # definition of the biconditional may look unusual compared to most # definitions, but it strictly satisfies these requirements. # # See <a href="dfbi1">dfbi1</a>, <a href="dfbi1">dfbi2</a>, and <a href="dfbi3">dfbi3</a> for theorems suggesting typical # textbook definitions of <->, showing that our definition has the # properties we expect. Theorem <a href="dfbi">dfbi</a> shows this definition rewritten # in an abbreviated form after conjunction is introduced. # </summary>
(/\ (-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph))) (-> (/\ (-> ph ps) (-> ps ph)) (<-> ph ps)))
def-bi-1 # <title> Biconditional Implies Two Conditionals </title>
(-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph)))
def-bi-2 # <title> Two Conditionals Implies Biconditional </title>
(-> (/\ (-> ph ps) (-> ps ph)) (<-> ph ps))
peirce # <title> Peirce's axiom </title> # <summary> # <a href="http://en.wikipedia.org/wiki/Charles_Sanders_Peirce">Peirce</a>'s # axiom. This odd-looking theorem is the "difference" between # an intuitionistic system of propositional calculus and a classical system # and is not accepted by intuitionists. When Peirce's axiom is added to an # intuitionistic system, the system becomes equivalent to our classical # system [[ax-1]] through [[ax-3]]. A curious fact about this # theorem is that it requires [[ax-3]] for its proof even though the # result has no negation connectives in it. # </summary>
(-> (-> (-> ph ps) ph) ph)
looinv # <title> Lukasiewicz's Inversion Axiom </title> # <summary> # The Inversion Axiom of the infinite-valued sentential logic (L-infinity) # of <a href="http://en.wikipedia.org/wiki/Jan_%C5%81ukasiewicz">Lukasiewicz</a>. # Using [[dfor2]], we can see that this essentially expresses # "disjunction commutes." # </summary>
(-> (-> (-> ph ps) ps) (-> (-> ps ph) ph))
notnot2 # <title> Double Negative </title>
(-> (-. (-. ph)) ph)
notnotri # <title> Double Negative </title>
(-. (-. ph))ph
notnot1 # <title> Double Negative </title>
(-> ph (-. (-. ph)))
notnoti # <title> Double Negative </title>
ph(-. (-. ph))
pm2.01 # <title> Reductio ad absurdum </title>
(-> (-> ph (-. ph)) (-. ph))
pm2.01d # <title> Reductio ad absurdum </title> # <summary> # The theorem <a href="pm2.01">pm2.01</a> written as an deduction. # </summary>
(-> ph (-> ps (-. ps)))(-> ph (-. ps))
(-> (-. (-> ph ps)) (-> (-. ph) ps))
(-> (-. (-> ph ps)) (-> ph (-. ps)))
(-> (-. (-> ph ps)) (-> (-. ph) (-. ps)))
(-> (-. (-> ph ps)) (-> ps ph))
mto # <title> Modus Tollens </title> # <table> # [ [ [ (-. [ ps) # (-> [ ph ] [ [ ps) # (-. [ ph ] ) ] ] # </table>
(-. ps) , (-> ph ps)(-. ph)
mtoi # <title> Modus Tollens </title> # <table> # [ [ [ (-. [ ch) # (-> ph (-> [ ps ] [ [ ch)) # (-> ph (-. [ ps ] ] ] )) # </table>
(-. ch) , (-> ph (-> ps ch))(-> ph (-. ps))
mtod # <title> Modus Tollens </title>
(-> ph (-. ch)) , (-> ph (-> ps ch))(-> ph (-. ps))
mt2 # <title> Modus Tollens </title>
ps , (-> ph (-. ps))(-. ph)
mt2i # <title> Modus Tollens </title>
ch , (-> ph (-> ps (-. ch)))(-> ph (-. ps))
mt2d # <title> Modus Tollens </title>
(-> ph ch) , (-> ph (-> ps (-. ch)))(-> ph (-. ps))
mt3 # <title> Modus Tollens </title>
(-. ps) , (-> (-. ph) ps)ph
mt3i # <title> Modus Tollens </title>
(-. ch) , (-> ph (-> (-. ps) ch))(-> ph ps)
mt3d # <title> Modus Tollens </title>
(-> ph (-. ch)) , (-> ph (-> (-. ps) ch))(-> ph ps)
mt4d # <title> Modus Tollens </title>
(-> ph ps) , (-> ph (-> (-. ch) (-. ps)))(-> ph ch)
nsyl # <title> Negated Syllogism </title>
(-> ph (-. ps)) , (-> ch ps)(-> ph (-. ch))
nsyld # <title> Negated Syllogism </title>
(-> ph (-> ps (-. ch))) , (-> ph (-> ta ch))(-> ph (-> ps (-. ta)))
nsyl2 # <title> Negated Syllogism </title>
(-> ph (-. ps)) , (-> (-. ch) ps)(-> ph ch)
nsyl3 # <title> Negated Syllogism </title>
(-> ph (-. ps)) , (-> ch ps)(-> ch (-. ph))
nsyl4 # <title> Negated Syllogism </title>
(-> ph ps) , (-> (-. ph) ch)(-> (-. ch) ps)
nsyl4t # <title> Negated Syllogism </title>
(-> (-> ph ps) (-> (-> (-. ph) ch) (-> (-. ch) ps)))
nsyli # <title> Negated Syllogism </title>
(-> ph (-> ps ch)) , (-> th (-. ch))(-> ph (-> th (-. ps)))
pm3.2im # <title> Join antecedents </title> # <summary> # This is the same as <a href="pm3.2">pm3.2</a>, but uses the primitive # connectives → and ¬ instead of conjunction. # </summary>
(-> ph (-> ps (-. (-> ph (-. ps)))))
(-> ph (-> (-. ps) (-. (-> ph ps))))
pm2.61 a.k.a cases # <title> Proof by cases </title>
(-> (-> ph ps) (-> (-> (-. ph) ps) ps))
cases # <title> Proof by cases </title>
(-> (-> ph ps) (-> (-> (-. ph) ps) ps))
casesi # <title> Proof by cases </title>
(-> ph ps) , (-> (-. ph) ps)ps
pm2.61i # <title> Proof by cases </title> # <table> # (-> ph [ ps) # (-> (-. ph) [ ps) # [ ps # </table>
(-> ph ps) , (-> (-. ph) ps)ps
casesd # <title> Proof by cases </title>
(-> ph (-> ps ch)) , (-> ph (-> (-. ps) ch))(-> ph ch)
pm2.61d # <title> Proof by cases </title>
(-> ph (-> ps ch)) , (-> ph (-> (-. ps) ch))(-> ph ch)
pm2.61d1 # <title> Eliminate an antecedent </title>
(-> ph (-> ps ch)) , (-> (-. ps) ch)(-> ph ch)
pm2.61d2 # <title> Eliminate an antecedent </title>
(-> ph (-> (-. ps) ch)) , (-> ps ch)(-> ph ch)
pm2.18i # <title> Proof by contradiction </title>
(-> (-. ph) ph)ph
pm2.61ii # <title> Eliminate an antecedent </title>
(-> (-. ph) (-> (-. ps) ch)) , (-> ph ch) , (-> ps ch)ch
pm2.61nii # <title> Eliminate an antecedent </title>
(-> ph (-> ps ch)) , (-> (-. ph) ch) , (-> (-. ps) ch)ch
pm2.61iii # <title> Eliminate an antecedent </title>
(-> (-. ph) (-> (-. ps) (-> (-. ch) th))) , (-> ph th) , (-> ps th) , (-> ch th)th
(-> (-> (-. ph) ps) (-> (-> ph ps) ps))
pm2.65 # <title> Proof by contradiction </title>
(-> (-> ph ps) (-> (-> ph (-. ps)) (-. ph)))
pm2.65i # <title> Proof by contradiction </title>
(-> ph ps) , (-> ph (-. ps))(-. ph)
pm2.65d # <title> Proof by contradiction </title>
(-> ph (-> ps ch)) , (-> ph (-> ps (-. ch)))(-> ph (-. ps))
ja # <title> Join the antecedents of two premises </title>
(-> (-. ph) ch) , (-> ps ch)(-> (-> ph ps) ch)
pm3.26im # <title> Simplification </title> # <summary> # This is the same as <a href="pm3.26">pm3.26</a>, but uses the primitive # connectives → and ¬ instead of conjunction. # </summary>
(-> (-. (-> ph (-. ps))) ph)
pm3.27im # <title> Simplification </title> # <summary> # This is the same as <a href="pm3.27">pm3.276</a>, but uses the primitive # connectives → and ¬ instead of conjunction. # </summary>
(-> (-. (-> ph (-. ps))) ps)
impt # <title> Importation theorem </title> # <summary> # This is the same as the <a href="imp">import theorem</a>, but uses the primitive # connectives → and ¬ instead of conjunction. # </summary>
(-> (-> ph (-> ps ch)) (-> (-. (-> ph (-. ps))) ch))
syldx # <title> Syllogism </title>
(-> ph (-> ps ch))(-> (-> ch th) (-> ph (-> ps th)))
expt # <title> Exportation theorem </title> # <summary> # This is the same as the <a href="exp">export theorem</a>, but uses the primitive # connectives → and ¬ instead of conjunction. # </summary>
(-> (-> (-. (-> ph (-. ps))) ch) (-> ph (-> ps ch)))
impi # <title> Importation Inference </title>
(-> ph (-> ps ch))(-> (-. (-> ph (-. ps))) ch)
expi # <title> Exportation Inference </title>
(-> (-. (-> ph (-. ps))) ch)(-> ph (-> ps ch))
bijust # <title> Bicondition Justification </title> # <summary> # Theorem used to justify the <a href="df-bi">definition of biconditional</a>. # </summary>
(-. (-> (-> ph ph) (-. (-> ph ph))))
df-bi # <title> Alternative Definition of Biconditional </title> # <summary> # See <a href="def-bi">def-bi</a> for more information. # </summary>
(-. (-> (-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) (-. (-> (-. (-> (-> ph ps) (-. (-> ps ph)))) (<-> ph ps)))))
bi1 # <title> Infer Left to Right </title> # <suggest> right('Infer', '→') </suggest>
(-> (<-> ph ps) (-> ph ps))
bi2 # <title> Infer Right to Left </title> # <suggest> right('Infer', '←') </suggest>
(-> (<-> ph ps) (-> ps ph))
bi3 # <title> Bicondition from two conditionals </title>
(-> (-> ph ps) (-> (-> ps ph) (<-> ph ps)))
biimpi a.k.a. bi1i? # <title> Biconditional Implies Conditional </title>
(<-> ph ps)(-> ph ps)
biimpri # <title> Biconditional Implies Conditional </title> # <table> # ((<-> <r> ph <g> ps)) (-> <g> ps <r> ph)) # </table>
(<-> ph ps)(-> ps ph)
biimpd # <title> Biconditional Implies Conditional </title>
(-> ph (<-> ps ch))(-> ph (-> ps ch))
biimprd # <title> Biconditional Implies Conditional </title>
(-> ph (<-> ps ch))(-> ph (-> ch ps))
biimpcd Getting a bit decadent here... just use biimpd com12! # <title> Biconditional Implies Conditional </title>
(-> ph (<-> ps ch))(-> ps (-> ph ch))
biimprcd # <title> Biconditional Implies Conditional </title>
(-> ph (<-> ps ch))(-> ch (-> ph ps))
def-bi-1i # <title> Biconditional Implies Two Conditionals </title>
(<-> ph ps)(/\ (-> ph ps) (-> ps ph))
def-bi-2i # <title> Two Conditionals Implies Biconditional </title>
(/\ (-> ph ps) (-> ps ph))(<-> ph ps)
impbii a.k.a. biconsi # <title> Bicondition from two conditionals </title> # <table> # (-> <r> ph <g> ps) # (-> <g> ps <r> ph) # (<-> <r> ph <g> ps) # </table>
(-> ph ps) , (-> ps ph)(<-> ph ps)
def-bi' # <title> Alternative Definition of Biconditional </title> # <summary # See <a href="def-bi">def-bi</a> for more information. This is the same as # See <a href="dfbi2">dfbi2</a>. # </summary>
(<-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph)))
df-an # <title> Definition of AND </title> # <summary> Define conjunction, logical AND. # This theorem is based on an earlier <a href="df-and">definition of AND</a> which # did not use the biconditional. This theorem writes the definition of AND in a more # familiar form using the biconditional. # </summary>
(<-> (/\ ph ps) (-. (-> ph (-. ps))))
bitri # <title> Transitive Property </title> # <table> # (<-> ph ] [ ps ] ] ) # [ (<-> [ ps ] [ ch) # (<-> ph ] [ [ [ ch) # </table>
(<-> ph ps) , (<-> ps ch)(<-> ph ch)
dfbi1 # <title> Bicondition Definition from primitive connectives </title>
(<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph)))))
bi2.04 There's no point in having this theorem if we're not going to prove it as described in prop.ghi. thm (dfbi1gb () () (<-> (<-> ph ps) (-. (-> (-> ph ps) (-. (-> ps ph))))) # No way! See the notes at http://us.metamath.org/mpegif/dfbi1gb.html ph ps dfbi1) # <title> Commute Antecedents </title>
(<-> (-> ph (-> ps ch)) (-> ps (-> ph ch)))
notnot # <title> Double Negative </title>
(<-> ph (-. (-. ph)))
notnotr # <title> Double Negative </title>
(<-> (-. (-. ph)) ph)
pm4.8 # <title> Proof by contradiction </title>
(<-> (-> ph (-. ph)) (-. ph))
pm4.81 # <title> Proof by contradiction </title>
(<-> (-> (-. ph) ph) ph)
con1b # <title> Contraposition </title> # <summary> Bidirectional version of <a href="con1">con1</a>. </summary>
(<-> (-> (-. ph) ps) (-> (-. ps) ph))
con2b # <title> Contraposition </title> # <summary> Bidirectional version of <a href="con2">con2</a>. </summary>
(<-> (-> ph (-. ps)) (-> ps (-. ph)))
con34b # <title> Contrapositive </title> # <suggest> right('Equivalence', '←') </suggest>
(<-> (-> ph ps) (-> (-. ps) (-. ph)))
pm5.4 # <title> Absorb Antecedent </title>
(<-> (-> ph (-> ph ps)) (-> ph ps))
imdi # <title> Distributive Property </title> # <suggest> right('Distribute', 'L') left('Distribute', '-L') </suggest>
(<-> (-> ph (-> ps ch)) (-> (-> ph ps) (-> ph ch)))
bicomi # <title> Commutative Property </title>
(<-> ph ps)(<-> ps ph)
pm5.41 # <title> Distributive Property </title>
(<-> (-> (-> ph ps) (-> ph ch)) (-> ph (-> ps ch)))
biid # <title> Identity </title>
(<-> ph ph)
biidd Decadent... # <title> Biconditional Identity <title>
(-> ph (<-> ps ps))
bitr2i # <title> Transitive Property </title>
(<-> ph ps) , (<-> ps ch)(<-> ch ph)
bitr3i # <title> Transitive Property </title> # <table> # (<-> ps ] [ ph ] ) # (<-> ps ] [ [ ch) # (<-> [ [ ph [ ch) # </table>
(<-> ps ph) , (<-> ps ch)(<-> ph ch)
bitr4i # <title> Transitive Property </title>
(<-> ph ps) , (<-> ch ps)(<-> ph ch)
3bitri # <title> Transitive Property </title>
(<-> ph ps) , (<-> ps ch) , (<-> ch th)(<-> ph th)
3bitrri # <title> Transitive Property </title>
(<-> ph ps) , (<-> ps ch) , (<-> ch th)(<-> th ph)
3bitr2i # <title> Transitive Property </title>
(<-> ph ps) , (<-> ch ps) , (<-> ch th)(<-> ph th)
3bitr2ri # <title> Transitive Property </title>
(<-> ph ps) , (<-> ch ps) , (<-> ch th)(<-> th ph)
3bitr3i This is getting boring... # <title> Transitive Property </title>
(<-> ph ps) , (<-> ph ch) , (<-> ps th)(<-> ch th)
3bitr3ri # <title> Transitive Property </title>
(<-> ph ps) , (<-> ph ch) , (<-> ps th)(<-> th ch)
3bitr4i # <title> Transitive Property </title>
(<-> ph ps) , (<-> ch ph) , (<-> th ps)(<-> ch th)
3bitr4ri # <title> Transitive Property </title>
(<-> ph ps) , (<-> ch ph) , (<-> th ps)(<-> th ch)
imbi2i Ok, some constructors # <title> Equivalence over Implication </title> # <table> # (<-> [ ph ] [ [ ps) # (<-> (-> ch [ ph ] ) [ (-> ch [ ps)) # </table>
(<-> ph ps)(<-> (-> ch ph) (-> ch ps))
imbi1i # <title> Equivalence over Implication </title> # <table> # (<-> ph ] ] [ ps ] ) # (<-> (-> ph ] ch) ] (-> [ ps ] ch)) # </table>
(<-> ph ps)(<-> (-> ph ch) (-> ps ch))
notbii # <title> Negation Both Sides </title> # <table> # (<-> [ ph ] [ ps ] ) # (<-> (-. [ ph ] ) (-. [ ps ] )) # </table>
(<-> ph ps)(<-> (-. ph) (-. ps))
imbi12i # <title> Join two equivalences to form equivalent implication </title>
(<-> ph ps) , (<-> ch th)(<-> (-> ph ch) (-> ps th))
mpbi # <title> Modus Ponens </title> # <table> # ph ] ] ] # (<-> ph ] [ ps ] ) # [ [ ps ] # </table>
ph , (<-> ph ps)ps
mpbir # <title> Modus Ponens </title> # <table> # [ [ ps ] # (<-> ph ] [ ps ] ) # ph ] ] ] # </table>
ps , (<-> ph ps)ph
mtbi # <title> Modus Tollens </title> # <table> # (-. [ ph ] ) ] ] # (<-> [ ph ] [ [ ps) # [ [ [ (-. [ ps) # </table>
(-. ph) , (<-> ph ps)(-. ps)
mtbir # <title> Modus Tollens </title> # <table> # [ [ (-. [ ps) # (<-> [ ph ] [ [ ps) # (-. [ ph) ] ] ] # </table>
(-. ps) , (<-> ph ps)(-. ph)
mpbii # <title> Modus Ponens </title> # <table> # [ ps ] # (-> ph (<-> [ ps ] ch)) # (-> ph [ [ ch)) # </table>
ps , (-> ph (<-> ps ch))(-> ph ch)
mpbiri # <title> Modus Ponens </title>
ch , (-> ph (<-> ps ch))(-> ph ps)
mpbid # <title> Modus Ponens </title>
(-> ph ps) , (-> ph (<-> ps ch))(-> ph ch)
mpbird # <title> Modus Ponens </title>
(-> ph ch) , (-> ph (<-> ps ch))(-> ph ps)
a1bi # <title> Theorem as antecedent </title> # <table> # [ ph ] # (<-> ps (-> [ ph ] ps)) # </table>
ph(<-> ps (-> ph ps))
sylib # <title> Syllogism </title> # <table> # (-> ph [ ps ] ] ] ) # [ (<-> ps ] [ ch ] ) # (-> ph [ [ [ ch ] ) # </table>
(-> ph ps) , (<-> ps ch)(-> ph ch)
sylbi # <title> Syllogism </title> # <table> # (<-> ph [ ps ] ] ] ) # [ (-> ps ] [ ch ] ) # ( -> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
sylibr # <title> Syllogism </title>
(-> ph ps) , (<-> ch ps)(-> ph ch)
sylbir # <title> Syllogism </title>
(<-> ps ph) , (-> ps ch)(-> ph ch)
sylibd # <title> Syllogism </title>
(-> ph (-> ps ch)) , (-> ph (<-> ch th))(-> ph (-> ps th))
sylbid # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (-> ph (-> ch th))(-> ph (-> ps th))
sylibrd # <title> Syllogism </title>
(-> ph (-> ps ch)) , (-> ph (<-> th ch))(-> ph (-> ps th))
sylbird # <title> Syllogism </title>
(-> ph (<-> ch ps)) , (-> ph (-> ch th))(-> ph (-> ps th))
syl5ib # <title> Syllogism </title>
(-> ph (-> ps ch)) , (<-> th ps)(-> ph (-> th ch))
syl5ibr # <title> Syllogism </title>
(-> ph (-> ps ch)) , (<-> ps th)(-> ph (-> th ch))
syl5bi # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (-> th ps)(-> ph (-> th ch))
syl5cbi # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (-> th ps)(-> th (-> ph ch))
syl5bir # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (-> th ch)(-> ph (-> th ps))
syl5cbir # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (-> th ch)(-> th (-> ph ps))
syl6ib # <title> Syllogism </title>
(-> ph (-> ps ch)) , (<-> ch th)(-> ph (-> ps th))
syl6ibr # <title> Syllogism </title>
(-> ph (-> ps ch)) , (<-> th ch)(-> ph (-> ps th))
syl6bi # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (-> ch th)(-> ph (-> ps th))
syl6bir # <title> Syllogism </title>
(-> ph (<-> ch ps)) , (-> ch th)(-> ph (-> ps th))
syl7ib # <title> Syllogism </title>
(-> ph (-> ps (-> ch th))) , (<-> ta ch)(-> ph (-> ps (-> ta th)))
syl8ib # <title> Syllogism </title>
(-> ph (-> ps (-> ch th))) , (<-> th ta)(-> ph (-> ps (-> ch ta)))
3imtr3i # <title> Syllogism </title>
(-> ph ps) , (<-> ph ch) , (<-> ps th)(-> ch th)
3imtr4i # <title> Syllogism </title>
(-> ph ps) , (<-> ch ph) , (<-> th ps)(-> ch th)
con1bii # <title> Contraposition </title>
(<-> (-. ph) ps)(<-> (-. ps) ph)
con2bii # <title> Contraposition </title>
(<-> ph (-. ps))(<-> ps (-. ph))
df-or # <title> Definition of OR </title> # <summary> # Define disjunction (logical 'or'). This is our first use of the # biconditional connective in a definition; we use it in place of the # traditional "<=def=>", which means the same thing, except that we can # manipulate the biconditional connective directly in proofs rather than # having to rely on an informal definition substitution rule. Note that # if we mechanically substitute #(-> (-. ph) ps)# for #(\/ ph ps)#, # we end up with an instance of previously proved <a href="biid">identity theorem</a>. This # is the justification for the definition, along with the fact that it # introduces a new symbol \/. # </summary>
(<-> (\/ ph ps) (-> (-. ph) ps))
pm4.64 # <title> Alternative Definition of OR </title>
(<-> (-> (-. ph) ps) (\/ ph ps))
pm2.54 # <title> Infer Disjunction </title>
(-> (-> (-. ph) ps) (\/ ph ps))
pm4.63 # <title> Alternative Definition of AND </title>
(<-> (-. (-> ph (-. ps))) (/\ ph ps))
dfor2-lemma # <title> Alternative Definition of OR Lemma </title>
(<-> (-> (-. ph) ps) (-> (-> ph ps) ps))
dfor2 # <title> Alternative Definition of OR </title # <summary> Logical 'or' expressed in terms of implication only. </summary>
(<-> (\/ ph ps) (-> (-> ph ps) ps))
ori # <title> Infer implication from disjunction </title>
(\/ ph ps)(-> (-. ph) ps)
orri # <title> Infer implication from disjunction </title>
(-> (-. ph) ps)(\/ ph ps)
ord # <title> Deduce implication from disjunction </title>
(-> ph (\/ ps ch))(-> ph (-> (-. ps) ch))
orrd # <title> Deduce implication from disjunction </title>
(-> ph (-> (-. ps) ch))(-> ph (\/ ps ch))
imor # <title> OR and → Equivalance </title> # <suggest> right('Equivalence', '∨') </suggest>
(<-> (-> ph ps) (\/ (-. ph) ps))
pm4.62 Not really sure why we want this in addition to imor # <title> OR and → Equivalance Negated </title>
(<-> (-> ph (-. ps)) (\/ (-. ph) (-. ps)))
pm4.66 Likewise, this one is a trivial corollary of pm4.64 # <title> OR and → Equivalance Negated </title>
(<-> (-> (-. ph) (-. ps)) (\/ ph (-. ps)))
iman # <title> AND and → Equivalance </title> # <suggest> right('Equivalence', '∧') </suggest>
(<-> (-> ph ps) (-. (/\ ph (-. ps))))
annim # <title> Conjunction in terms of implication </title>
(<-> (/\ ph (-. ps)) (-. (-> ph ps)))
pm4.61 # <title> Conjunction in terms of implication </title>
(<-> (-. (-> ph ps)) (/\ ph (-. ps)))
pm4.65 # <title> Conjunction in terms of implication negated </title>
(<-> (-. (-> (-. ph) ps)) (/\ (-. ph) (-. ps)))
pm4.67 # <title> Conjunction in terms of implication negated </title>
(<-> (-. (-> (-. ph) (-. ps))) (/\ (-. ph) ps))
imnan # <title> Implication in terms of conjunction </title>
(<-> (-> ph (-. ps)) (-. (/\ ph ps)))
oridm # <title> Disjunction is Idempotent </title> # <suggest> right('Simplify', '∨') </suggest>
(<-> (\/ ph ph) ph)
pm4.25 # <title> Disjunction is Idempotent </title>
(<-> ph (\/ ph ph))
pm1.2 # <title> Disjunction is Idempotent </title>
(-> (\/ ph ph) ph)
orcom # <title> Commutative Property of OR </title> # <table> # (<-> (\/ <r> ph <g> ps) (\/ <g> ps <r> ph)) # </table>
(<-> (\/ ph ps) (\/ ps ph))
pm1.4 # <title> Commutative Property of OR </title>
(-> (\/ ph ps) (\/ ps ph))
pm2.62 # <title> Unidirectional definition of OR </title>
(-> (\/ ph ps) (-> (-> ph ps) ps))
pm2.621 # <title> Unidirectional definition of OR </title>
(-> (-> ph ps) (-> (\/ ph ps) ps))
pm2.68 # <title> Unidirectional definition of OR </title>
(-> (-> (-> ph ps) ps) (\/ ph ps))
orel1 # <title> Denial of a Disjunct </title> # <summary> Elimination of disjunction by denying a disjunct. <.summary>
(-> (-. ph) (-> (\/ ph ps) ps))
orel2 # <title> Denial of a Disjunct </title> # <summary> Elimination of disjunction by denying a disjunct. <.summary>
(-> (-. ph) (-> (\/ ps ph) ps))
(\/ ph (-> (\/ ph ps) ps))
(-> (\/ ph ps) (-> (-. ph) ps))
orbi2i # <title> Equivalence over Disjunction </title> # <table> # (<-> [ ph ] [ [ ps) # (<-> (\/ ch [ ph ] ) [ (\/ ch [ ps)) # </table>
(<-> ph ps)(<-> (\/ ch ph) (\/ ch ps))
orbi1i # <title> Equivalence over Disjunction </title> # <table> # (<-> ph ] ] [ ps ] ) # (<-> (\/ ph ] ch) ] (\/ [ ps ] ch)) # </table>
(<-> ph ps)(<-> (\/ ph ch) (\/ ps ch))
orbi12i # <title> Infer the disjunction of two equivalences </title>
(<-> p0 p1) , (<-> q0 q1)(<-> (\/ p0 q0) (\/ p1 q1))
or12 # <title> Rearrangement of disjuncts </title>
(<-> (\/ ph (\/ ps ch)) (\/ ps (\/ ph ch)))
pm1.5 # <title> Rearrangement of disjuncts </title>
(-> (\/ ph (\/ ps ch)) (\/ ps (\/ ph ch)))
orass # <title> Associative Property of OR </title> # <suggest> right('Associate', 'R') left('Associate', 'L') </suggest>
(<-> (\/ (\/ ph ps) ch) (\/ ph (\/ ps ch)))
pm2.31 # <title> Associatative Property of OR </title>
(-> (\/ ph (\/ ps ch)) (\/ (\/ ph ps) ch))
pm2.32 # <title> Associatative Property of OR </title>
(-> (\/ (\/ ph ps) ch) (\/ ph (\/ ps ch)))
or23 # <title> Rearrangement of disjuncts </title>
(<-> (\/ (\/ ph ps) ch) (\/ (\/ ph ch) ps))
or4 # <title> Rearrangement of disjuncts </title>
(<-> (\/ (\/ ph ps) (\/ ch th)) (\/ (\/ ph ch) (\/ ps th)))
or42 # <title> Rearrangement of disjuncts </title>
(<-> (\/ (\/ ph ps) (\/ ch th)) (\/ (\/ ph ch) (\/ th ps)))
orordi # <title> Distribution of disjunction over disjunction </title>
(<-> (\/ ph (\/ ps ch)) (\/ (\/ ph ps) (\/ ph ch)))
olc # <title> Introduction of a disjunct </title>
(-> ph (\/ ps ph))
orc # <title> Introduction of a disjunct </title>
(-> ph (\/ ph ps))
olci # <title> Introduction of a disjunct </title>
ph(\/ ps ph)
orci # <title> Introduction of a disjunct </title>
ph(\/ ph ps)
orcd # <title> Introduction of a disjunct </title>
(-> ph ps)(-> ph (\/ ps ch))
olcd # <title> Introduction of a disjunct </title>
(-> ph ps)(-> ph (\/ ch ps))
orcs # <title> Eliminate a Disjunct </title>
(-> (\/ ph ps) ch)(-> ph ch)
olcs # <title> Eliminate a Disjunct </title>
(-> (\/ ph ps) ch)(-> ps ch)
pm2.07 # <title> Disjunction is Idempotent </title>
(-> ph (\/ ph ph))
orordir Distribution of disjunction over disjunction. # <title> Distribution of disjunction over disjunction </title>
(<-> (\/ (\/ ph ps) ch) (\/ (\/ ph ch) (\/ ps ch)))
pm2.45 Theorem *2.45 of [bib/WhiteheadRussell] p. 106. # <title> Eliminate a Disjunct </title>
(-> (-. (\/ ph ps)) (-. ph))
pm2.46 Theorem *2.46 of [bib/WhiteheadRussell] p. 106. # <title> Eliminate a Disjunct </title>
(-> (-. (\/ ph ps)) (-. ps))
pm2.47 Theorem *2.47 of [bib/WhiteheadRussell] p. 107.
(-> (-. (\/ ph ps)) (\/ (-. ph) ps))
pm2.48 Theorem *2.48 of [bib/WhiteheadRussell] p. 107.
(-> (-. (\/ ph ps)) (\/ ph (-. ps)))
pm2.49 Theorem *2.49 of [bib/WhiteheadRussell] p. 107.
(-> (-. (\/ ph ps)) (\/ (-. ph) (-. ps)))
pm2.67 Theorem *2.67 of [bib/WhiteheadRussell] p. 107. # <title> Eliminate a Disjunct </title>
(-> (-> (\/ ph ps) ps) (-> ph ps))
pm3.2 Join antecedents with conjunction. Theorem *3.2 of [bib/WhiteheadRussell] p. 111. # <title> Join antecedents with conjunction </title>
(-> ph (-> ps (/\ ph ps)))
pm3.21 Join antecedents with conjunction. Theorem *3.21 of [bib/WhiteheadRussell] p. 111. # <title> Join antecedents with conjunction </title>
(-> ph (-> ps (/\ ps ph)))
pm3.37 Theorem *3.37 (Transp) of [bib/WhiteheadRussell] p. 112.
(-> (-> (/\ ph ps) ch) (-> (/\ ph (-. ch)) (-. ps)))
pm3.43i # <title> Nested conjunction of antecedents </title>
(-> (-> ph ps) (-> (-> ph ch) (-> ph (/\ ps ch))))
jca # <title> Join two implications </title> # <table> # (-> ph ps ] ] ) # (-> ph ] [ ch) # (-> ph (/\ ps ] [ ch)) # </table>
(-> ph ps) , (-> ph ch)(-> ph (/\ ps ch))
jca31 Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.) # <title> Join three implications </title>
(-> ph ps) , (-> ph ch) , (-> ph th)(-> ph (/\ (/\ ps ch) th))
jca32 Join three consequents. (Contributed by FL, 1-Aug-2009.) # <title> Join three implications </title>
(-> ph ps) , (-> ph ch) , (-> ph th)(-> ph (/\ ps (/\ ch th)))
jcai # <title> Replace implication with conjunction </title>
(-> ph ps) , (-> ph (-> ps ch))(-> ph (/\ ps ch))
jctl Inference conjoining a theorem to the left of a consequent. # <title> Add theorem to the left of a consequent </title>
ps(-> ph (/\ ps ph))
jctr Inference conjoining a theorem to the right of a consequent. # <title> Add theorem to the right of a consequent </title>
ps(-> ph (/\ ph ps))
jctil # <title> Add theorem to the left of a consequent </title>
(-> ph ps) , ch(-> ph (/\ ch ps))
jctir # <title> Add theorem to the right of a consequent </title>
(-> ph ps) , ch(-> ph (/\ ps ch))
ancl # <title> Add antecedent </title>
(-> (-> ph ps) (-> ph (/\ ph ps)))
ancr # <title> Add antecedent </title>
(-> (-> ph ps) (-> ph (/\ ps ph)))
ancli Deduction conjoining antecedent to left of consequent. # <title> Add Antecedent </title> # <table> # (-> ph [ [ ps) # (-> ph [ (/\ ph [ ps)) # </table>
(-> ph ps)(-> ph (/\ ph ps))
ancri Deduction conjoining antecedent to right of consequent. # <title> Add Antecedent </title> # <table> # (-> ph [ ps ] ) # (-> ph (/\ [ ps ] ph)) # </table>
(-> ph ps)(-> ph (/\ ps ph))
ancld Deduction conjoining antecedent to left of consequent in nested implication. # <title> Add Antecedent </title>
(-> ph (-> ps ch))(-> ph (-> ps (/\ ps ch)))
ancrd Deduction conjoining antecedent to right of consequent in nested implication. # <title> Add Antecedent </title>
(-> ph (-> ps ch))(-> ph (-> ps (/\ ch ps)))
anc2l Conjoin antecedent to left of consequent in nested implication. # <title> Add Antecedent </title>
(-> (-> ph (-> ps ch)) (-> ph (-> ps (/\ ph ch))))
anc2r Conjoin antecedent to right of consequent in nested implication. # <title> Add Antecedent </title>
(-> (-> ph (-> ps ch)) (-> ph (-> ps (/\ ch ph))))
anc2li Deduction conjoining antecedent to left of consequent in nested implication. # <title> Add Antecedent </title>
(-> ph (-> ps ch))(-> ph (-> ps (/\ ph ch)))
anc2ri Deduction conjoining antecedent to right of consequent in nested implication. # <title> Add Antecedent </title>
(-> ph (-> ps ch))(-> ph (-> ps (/\ ch ph)))
anor Conjunction in terms of disjunction (DeMorgan's law). Theorem *4.5 of [bib/WhiteheadRussell] p. 120. # <title> DeMorgan's law </title> # <summary> # <a href="http://en.wikipedia.org/wiki/Augustus_De_Morgan">De Morgan</a>'s law # describing conjunction in terms of disjunction. For an alternative form see # <a href="oran">oran</a>. # </summary>
(<-> (/\ ph ps) (-. (\/ (-. ph) (-. ps))))
ianor Negated conjunction in terms of disjunction (DeMorgan's law). Theorem *4.51 of [bib/WhiteheadRussell] p. 120. # <title> DeMorgan's law </title> # <summary> # <a href="http://en.wikipedia.org/wiki/Augustus_De_Morgan">De Morgan</a>'s law # describing conjunction in terms of disjunction. For the non-negated form see # <a href="anor">anor</a>. # </summary>
(<-> (-. (/\ ph ps)) (\/ (-. ph) (-. ps)))
ioran Negated disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.56 of [bib/WhiteheadRussell] p. 120. # <title> DeMorgan's law </title> # <summary> # <a href="http://en.wikipedia.org/wiki/Augustus_De_Morgan">De Morgan</a>'s law # describing disjunction in terms of conjunction. For the non-negated form see # <a href="oran">oran</a>. # </summary>
(<-> (-. (\/ ph ps)) (/\ (-. ph) (-. ps)))
pm4.52 Theorem *4.52 of [bib/WhiteheadRussell] p. 120. # <title> Collary of DeMorgan's law </title>
(<-> (/\ ph (-. ps)) (-. (\/ (-. ph) ps)))
pm4.53 Theorem *4.53 of [bib/WhiteheadRussell] p. 120. # <title> Collary of DeMorgan's law </title>
(<-> (-. (/\ ph (-. ps))) (\/ (-. ph) ps))
pm4.54 Theorem *4.54 of [bib/WhiteheadRussell] p. 120. # <title> Collary of DeMorgan's law </title>
(<-> (/\ (-. ph) ps) (-. (\/ ph (-. ps))))
pm4.55 Theorem *4.55 of [bib/WhiteheadRussell] p. 120. # <title> Collary of DeMorgan's law </title>
(<-> (-. (/\ (-. ph) ps)) (\/ ph (-. ps)))
pm4.56 Theorem *4.56 of [bib/WhiteheadRussell] p. 120. # <title> Collary of DeMorgan's law </title>
(<-> (/\ (-. ph) (-. ps)) (-. (\/ ph ps)))
oran Disjunction in terms of conjunction (DeMorgan's law). Compare Theorem *4.57 of [bib/WhiteheadRussell] p. 120. # <title> DeMorgan's law </title> # <summary> # <a href="http://en.wikipedia.org/wiki/Augustus_De_Morgan">De Morgan</a>'s law # describing disjunction in terms of conjunction. For an alternative form see # <a href="anor">anor</a>. # </summary>
(<-> (\/ ph ps) (-. (/\ (-. ph) (-. ps))))
pm4.57 Theorem *4.57 of [bib/WhiteheadRussell] p. 120. # <title> Collary of DeMorgan's law </title>
(<-> (-. (/\ (-. ph) (-. ps))) (\/ ph ps))
pm3.1 Theorem *3.1 of [bib/WhiteheadRussell] p. 111. # <title> Collary of DeMorgan's law </title>
(-> (/\ ph ps) (-. (\/ (-. ph) (-. ps))))
pm3.11 Theorem *3.11 of [bib/WhiteheadRussell] p. 111. # <title> Collary of DeMorgan's law </title>
(-> (-. (\/ (-. ph) (-. ps))) (/\ ph ps))
pm3.12 Theorem *3.12 of [bib/WhiteheadRussell] p. 111. # <title> Both are true or one is false </title>
(\/ (\/ (-. ph) (-. ps)) (/\ ph ps))
pm3.13 Theorem *3.13 of [bib/WhiteheadRussell] p. 111. # <title> If both are not true then one is false </title>
(-> (-. (/\ ph ps)) (\/ (-. ph) (-. ps)))
pm3.14 Theorem *3.14 of [bib/WhiteheadRussell] p. 111. # <title> If one is false, then both are not true </title>
(-> (\/ (-. ph) (-. ps)) (-. (/\ ph ps)))
pm3.26 Elimination of a conjunct. Theorem *3.26 (Simp) of [bib/WhiteheadRussell] p. 112. # <title> 'Remove Right Side of AND' </title> # <suggest> right('Remove', 'L') </suggest>
(-> (/\ ph ps) ph)
pm3.26i Inference eliminating a conjunct. # <title> 'Remove Right Side of AND' </title>
(/\ ph ps)ph
pm3.26d Deduction eliminating a conjunct. # <title> 'Remove Right Side of AND' </title>
(-> ph (/\ ps ch))(-> ph ps)
pm3.26bi Deduction eliminating a conjunct. # <title> 'Remove Right Side of AND' </title>
(<-> ph (/\ ps ch))(-> ph ps)
pm3.27 Elimination of a conjunct. Theorem *3.27 (Simp) of [bib/WhiteheadRussell] p. 112. # <title> Remove Left Side of AND </title>
(-> (/\ ph ps) ps)
pm3.27i Inference eliminating a conjunct. # <title> Remove Left Side of AND </title>
(/\ ph ps)ps
pm3.27d Deduction eliminating a conjunct. # <title> Remove Left Side of AND </title>
(-> ph (/\ ps ch))(-> ph ch)
pm3.27bi Deduction eliminating a conjunct. # <title> Remove Left Side of AND </title>
(<-> ph (/\ ps ch))(-> ph ch)
pm3.41 Theorem *3.41 of [bib/WhiteheadRussell] p. 113. # <title> Add to Antecedent </title>
(-> (-> ph ch) (-> (/\ ph ps) ch))
pm3.42 Theorem *3.42 of [bib/WhiteheadRussell] p. 113. # <title> Add to Antecedent </title>
(-> (-> ps ch) (-> (/\ ph ps) ch))
pm3.41i # <title> Add to Antecedent </title> # <table> # (-> ph ] ] ps) # (-> (/\ ph ] ch) ] ps) # </table>
(-> ph ps)(-> (/\ ph ch) ps)
pm3.42i # <title> Add to Antecedent </title> # <table> # (-> [ ph ps) # (-> (/\ ch [ ph) ps) # </table>
(-> ph ps)(-> (/\ ch ph) ps)
anclb Conjoin antecedent to left of consequent. Theorem *4.7 of [bib/WhiteheadRussell] p. 120. # <title> Add Antecedent as consequent </title>
(<-> (-> ph ps) (-> ph (/\ ph ps)))
ancrb Conjoin antecedent to right of consequent. # <title> Add Antecedent as consequent </title>
(<-> (-> ph ps) (-> ph (/\ ps ph)))
pm3.4 Conjunction implies implication. Theorem *3.4 of [bib/WhiteheadRussell] p. 113. # <title> Conjunction implies implication </title>
(-> (/\ ph ps) (-> ph ps))
pm4.45im Conjunction with implication. Compare Theorem *4.45 of [bib/WhiteheadRussell] p. 119. # <title> Conjunction with implication </title>
(<-> ph (/\ ph (-> ps ph)))
anim12i Conjoin antecedents and consequents of two premises. # <title> Join antecedents and consequents </title>
(-> ph ps) , (-> ch th)(-> (/\ ph ch) (/\ ps th))
anim1i Introduce conjunct to both sides of an implication. # <title> Introduce conjunct to both sides </title>
(-> ph ps)(-> (/\ ph ch) (/\ ps ch))
anim2i Introduce conjunct to both sides of an implication. # <title> Introduce conjunct to both sides </title>
(-> ph ps)(-> (/\ ch ph) (/\ ch ps))
orim12i Disjoin antecedents and consequents of two premises. # <title> Join antecedents and consequents </title>
(-> ph ps) , (-> ch th)(-> (\/ ph ch) (\/ ps th))
orim1i Introduce disjunct to both sides of an implication. # <title> Introduce disjunct to both sides </title>
(-> ph ps)(-> (\/ ph ch) (\/ ps ch))
orim2i Introduce disjunct to both sides of an implication. # <title> Introduce disjunct to both sides </title>
(-> ph ps)(-> (\/ ch ph) (\/ ch ps))
pm2.3 Theorem *2.3 of [bib/WhiteheadRussell] p. 104.
(-> (\/ ph (\/ ps ch)) (\/ ph (\/ ch ps)))
jao Disjunction of antecedents. Compare Theorem *3.44 of [bib/WhiteheadRussell] p. 113. # <title> Disjunction of antecedents </title>
(-> (-> ph ps) (-> (-> ch ps) (-> (\/ ph ch) ps)))
jaoi Inference disjoining the antecedents of two implications. # <title> Join two implications </title> # <table> # (-> ph ] ] ] ps) # (-> [ [ ch ] ps) # (-> (\/ ph ] [ ch ] ) ps) # </table>
(-> ph ps) , (-> ch ps)(-> (\/ ph ch) ps)
pm2.41 Theorem *2.41 of [bib/WhiteheadRussell] p. 106. # <title> Remove Repeated Disjunct </title>
(-> (\/ ps (\/ ph ps)) (\/ ph ps))
pm2.42 Theorem *2.42 of [bib/WhiteheadRussell] p. 106. # <title> Remove Disjunct </title>
(-> (\/ (-. ph) (-> ph ps)) (-> ph ps))
pm2.4 Theorem *2.4 of [bib/WhiteheadRussell] p. 106. # <title> Remove Repeated Disjunct </title>
(-> (\/ ph (\/ ph ps)) (\/ ph ps))
pm4.44 Theorem *4.44 of [bib/WhiteheadRussell] p. 119. # <title> Extra Conjunct </title> # <suggest> left('Simplify', '∨') </suggest>
(<-> ph (\/ ph (/\ ph ps)))
pm5.63 Theorem *5.63 of [bib/WhiteheadRussell] p. 125.
(<-> (\/ ph ps) (\/ ph (/\ (-. ph) ps)))
impexp Import-export theorem. Part of Theorem *4.87 of [bib/WhiteheadRussell] p. 122. # <title> Import-Export Theorem </title> # <suggest> left('Equivalence', '∧→') right('Equivalence', '→→') </suggest>
(<-> (-> (/\ ph ps) ch) (-> ph (-> ps ch)))
pm3.3 Theorem *3.3 (Exp) of [bib/WhiteheadRussell] p. 112. # <title> Export Theorem Collary </title>
(-> (-> (/\ ph ps) ch) (-> ph (-> ps ch)))
pm3.31 Theorem *3.31 (Imp) of [bib/WhiteheadRussell] p. 112. # <title> Import Theorem </title>
(-> (-> ph (-> ps ch)) (-> (/\ ph ps) ch))
imp Importation inference. (The proof was shortened by Eric Schmidt, 22-Dec-2006.) # <title> Import Theorem </title>
(-> ph (-> ps ch))(-> (/\ ph ps) ch)
impcom Importation inference with commuted antecedents. # <title> Import & Commute </title>
(-> ph (-> ps ch))(-> (/\ ps ph) ch)
pm4.14 Theorem *4.14 of [bib/WhiteheadRussell] p. 117.
(<-> (-> (/\ ph ps) ch) (-> (/\ ph (-. ch)) (-. ps)))
pm4.15 Theorem *4.15 of [bib/WhiteheadRussell] p. 117.
(<-> (-> (/\ ph ps) (-. ch)) (-> (/\ ps ch) (-. ph)))
pm4.78 Theorem *4.78 of [bib/WhiteheadRussell] p. 121. # <title> Distributive Property </title> # <suggest> right('Distribute', '-R') </suggest>
(<-> (\/ (-> ph ps) (-> ph ch)) (-> ph (\/ ps ch)))
pm4.79 Theorem *4.79 of [bib/WhiteheadRussell] p. 121. # <title> Distributive Property </title> # <suggest> right('Distribute', '-L') </suggest>
(<-> (\/ (-> ps ph) (-> ch ph)) (-> (/\ ps ch) ph))
pm4.87 Theorem *4.87 of [bib/WhiteheadRussell] p. 122. (The proof was shortened by Eric Schmidt, 26-Oct-2006.) # <title> Import-Export Theorem </title>
(/\ (/\ (<-> (-> (/\ ph ps) ch) (-> ph (-> ps ch))) (<-> (-> ph (-> ps ch)) (-> ps (-> ph ch)))) (<-> (-> ps (-> ph ch)) (-> (/\ ps ph) ch)))
pm3.33 Theorem *3.33 (Syll) of [bib/WhiteheadRussell] p. 112. # <title> Syllogism </title>
(-> (/\ (-> ph ps) (-> ps ch)) (-> ph ch))
pm3.34 Theorem *3.34 (Syll) of [bib/WhiteheadRussell] p. 112. # <title> Syllogism </title>
(-> (/\ (-> ps ch) (-> ph ps)) (-> ph ch))
pm3.35 Conjunctive detachment. Theorem *3.35 of [bib/WhiteheadRussell] p. 112. # <title> Conjunctive detachment </title> # <suggest> right('Simplify', '→') </suggest>
(-> (/\ ph (-> ph ps)) ps)
pm5.31 Theorem *5.31 of [bib/WhiteheadRussell] p. 125.
(-> (/\ ch (-> ph ps)) (-> ph (/\ ps ch)))
imp3a # <title> Import Deduction </title>
(-> ph (-> ps (-> ch th)))(-> ph (-> (/\ ps ch) th))
imp31 # <title> Import Inference </title>
(-> ph (-> ps (-> ch th)))(-> (/\ (/\ ph ps) ch) th)
imp32 # <title> Import Inference </title>
(-> ph (-> ps (-> ch th)))(-> (/\ ph (/\ ps ch)) th)
imp4a # <title> Import Inference </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> ph (-> ps (-> (/\ ch th) ta)))
imp4b # <title> Import Inference </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> (/\ ph ps) (-> (/\ ch th) ta))
imp4c # <title> Import Inference </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> ph (-> (/\ (/\ ps ch) th) ta))
imp4d # <title> Import Inference </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> ph (-> (/\ ps (/\ ch th)) ta))
imp41 # <title> Import Inference </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> (/\ (/\ (/\ ph ps) ch) th) ta)
imp42 # <title> Import Inference </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> (/\ (/\ ph (/\ ps ch)) th) ta)
imp43 # <title> Import Inference </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> (/\ (/\ ph ps) (/\ ch th)) ta)
imp44 # <title> Import Inference </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> (/\ ph (/\ (/\ ps ch) th)) ta)
imp45 # <title> Import Inference </title>
(-> ph (-> ps (-> ch (-> th ta))))(-> (/\ ph (/\ ps (/\ ch th))) ta)
ex # <title> Export Inference </title>
(-> (/\ ph ps) ch)(-> ph (-> ps ch))
expcom # <title> Export & Commute </title>
(-> (/\ ph ps) ch)(-> ps (-> ph ch))
expimpd # <title> Export & Import </title>
(-> (/\ ph ps) (-> ch th))(-> ph (-> (/\ ps ch) th))
exp3a # <title> Export Deduction </title>
(-> ph (-> (/\ ps ch) th))(-> ph (-> ps (-> ch th)))
expdimp # <title> Export & Import </title>
(-> ph (-> (/\ ps ch) th))(-> (/\ ph ps) (-> ch th))
exp31 # <title> Export Inference </title>
(-> (/\ (/\ ph ps) ch) th)(-> ph (-> ps (-> ch th)))
exp32 # <title> Export Inference </title>
(-> (/\ ph (/\ ps ch)) th)(-> ph (-> ps (-> ch th)))
exp4a # <title> Export Inference </title>
(-> ph (-> ps (-> (/\ ch th) ta)))(-> ph (-> ps (-> ch (-> th ta))))
exp4b # <title> Export Inference </title>
(-> (/\ ph ps) (-> (/\ ch th) ta))(-> ph (-> ps (-> ch (-> th ta))))
exp4c # <title> Export Inference </title>
(-> ph (-> (/\ (/\ ps ch) th) ta))(-> ph (-> ps (-> ch (-> th ta))))
exp4d # <title> Export Inference </title>
(-> ph (-> (/\ ps (/\ ch th)) ta))(-> ph (-> ps (-> ch (-> th ta))))
exp41 # <title> Export Inference </title>
(-> (/\ (/\ (/\ ph ps) ch) th) ta)(-> ph (-> ps (-> ch (-> th ta))))
exp42 # <title> Export Inference </title>
(-> (/\ (/\ ph (/\ ps ch)) th) ta)(-> ph (-> ps (-> ch (-> th ta))))
exp43 # <title> Export Inference </title>
(-> (/\ (/\ ph ps) (/\ ch th)) ta)(-> ph (-> ps (-> ch (-> th ta))))
exp44 # <title> Export Inference </title>
(-> (/\ ph (/\ (/\ ps ch) th)) ta)(-> ph (-> ps (-> ch (-> th ta))))
exp45 # <title> Export Inference </title>
(-> (/\ ph (/\ ps (/\ ch th))) ta)(-> ph (-> ps (-> ch (-> th ta))))
impac Importation with conjunction in consequent. # <title> Import Inference </title>
(-> ph (-> ps ch))(-> (/\ ph ps) (/\ ch ps))
adantl # <title> Add Conjunct </title> # <table> # (-> [ ph [ ps) # (-> (/\ ch [ ph) [ ps) # </table>
(-> ph ps)(-> (/\ ch ph) ps)
adantr # <title> Add Conjunct </title> # <table> # (-> ph ] [ [ [ ps) # (-> (/\ ph ] [ ch ] ) [ ps) # </table>
(-> ph ps)(-> (/\ ph ch) ps)
adantld Deduction adding a conjunct to the left of an antecedent. # <title> Add Conjunct </title>
(-> ph (-> ps ch))(-> ph (-> (/\ th ps) ch))
adantrd Deduction adding a conjunct to the right of an antecedent. # <title> Add Conjunct </title>
(-> ph (-> ps ch))(-> ph (-> (/\ ps th) ch))
adantll Deduction adding a conjunct to antecedent. # <title> Add Conjunct </title>
(-> (/\ ph ps) ch)(-> (/\ (/\ th ph) ps) ch)
adantlr Deduction adding a conjunct to antecedent. # <title> Add Conjunct </title>
(-> (/\ ph ps) ch)(-> (/\ (/\ ph th) ps) ch)
adantrl Deduction adding a conjunct to antecedent. # <title> Add Conjunct </title>
(-> (/\ ph ps) ch)(-> (/\ ph (/\ th ps)) ch)
adantrr Deduction adding a conjunct to antecedent. # <title> Add Conjunct </title>
(-> (/\ ph ps) ch)(-> (/\ ph (/\ ps th)) ch)
adantlll Deduction adding a conjunct to antecedent. # <title> Add Conjunct </title>
(-> (/\ (/\ ph ps) ch) th)(-> (/\ (/\ (/\ ta ph) ps) ch) th)
adantllr Deduction adding a conjunct to antecedent. # <title> Add Conjunct </title>
(-> (/\ (/\ ph ps) ch) th)(-> (/\ (/\ (/\ ph ta) ps) ch) th)
adantlrl Deduction adding a conjunct to antecedent. # <title> Add Conjunct </title>
(-> (/\ (/\ ph ps) ch) th)(-> (/\ (/\ ph (/\ ta ps)) ch) th)
adantlrr Deduction adding a conjunct to antecedent. # <title> Add Conjunct </title>
(-> (/\ (/\ ph ps) ch) th)(-> (/\ (/\ ph (/\ ps ta)) ch) th)
adantrll Deduction adding a conjunct to antecedent. # <title> Add Conjunct </title>
(-> (/\ ph (/\ ps ch)) th)(-> (/\ ph (/\ (/\ ta ps) ch)) th)
adantrlr Deduction adding a conjunct to antecedent. # <title> Add Conjunct </title>
(-> (/\ ph (/\ ps ch)) th)(-> (/\ ph (/\ (/\ ps ta) ch)) th)
adantrrl Deduction adding a conjunct to antecedent. # <title> Add Conjunct </title>
(-> (/\ ph (/\ ps ch)) th)(-> (/\ ph (/\ ps (/\ ta ch))) th)
adantrrr Deduction adding a conjunct to antecedent. # <title> Add Conjunct </title>
(-> (/\ ph (/\ ps ch)) th)(-> (/\ ph (/\ ps (/\ ch ta))) th)
ad2antrr Deduction adding conjuncts to antecedent. # <title> Add Conjuncts </title>
(-> ph ps)(-> (/\ (/\ ph ch) th) ps)
ad2antlr Deduction adding conjuncts to antecedent. # <title> Add Conjuncts </title>
(-> ph ps)(-> (/\ (/\ ch ph) th) ps)
ad2antrl Deduction adding conjuncts to antecedent. # <title> Add Conjuncts </title>
(-> ph ps)(-> (/\ ch (/\ ph th)) ps)
ad2antll Deduction adding conjuncts to antecedent. # <title> Add Conjuncts </title>
(-> ph ps)(-> (/\ ch (/\ th ph)) ps)
ad2ant2l Deduction adding two conjuncts to antecedent. # <title> Add Conjuncts </title>
(-> (/\ ph ps) ch)(-> (/\ (/\ th ph) (/\ ta ps)) ch)
ad2ant2r Deduction adding two conjuncts to antecedent. # <title> Add Conjuncts </title>
(-> (/\ ph ps) ch)(-> (/\ (/\ ph th) (/\ ps ta)) ch)
ad2ant2lr Deduction adding two conjuncts to antecedent. # <title> Add Conjuncts </title>
(-> (/\ ph ps) ch)(-> (/\ (/\ th ph) (/\ ps ta)) ch)
ad2ant2rl Deduction adding two conjuncts to antecedent. # <title> Add Conjuncts </title>
(-> (/\ ph ps) ch)(-> (/\ (/\ ph th) (/\ ta ps)) ch)
simpll # <title> Simplify: Remove two conjuncts </title>
(-> (/\ (/\ ph ps) ch) ph)
simplr # <title> Simplify: Remove two conjuncts </title>
(-> (/\ (/\ ph ps) ch) ps)
simprl # <title> Simplify: Remove two conjuncts </title>
(-> (/\ ph (/\ ps ch)) ps)
simprr # <title> Simplify: Remove two conjuncts </title>
(-> (/\ ph (/\ ps ch)) ch)
simplll # <title> Simplify: Remove three conjuncts </title>
(-> (/\ (/\ (/\ ph ps) ch) th) ph)
simpllr # <title> Simplify: Remove three conjuncts </title>
(-> (/\ (/\ (/\ ph ps) ch) th) ps)
simplrl # <title> Simplify: Remove three conjuncts </title>
(-> (/\ (/\ ph (/\ ps ch)) th) ps)
simplrr # <title> Simplify: Remove three conjuncts </title>
(-> (/\ (/\ ph (/\ ps ch)) th) ch)
simprll # <title> Simplify: Remove three conjuncts </title>
(-> (/\ ph (/\ (/\ ps ch) th)) ps)
simprlr # <title> Simplify: Remove three conjuncts </title>
(-> (/\ ph (/\ (/\ ps ch) th)) ch)
simprrl # <title> Simplify: Remove three conjuncts </title>
(-> (/\ ph (/\ ps (/\ ch th))) ch)
simprrr # <title> Simplify: Remove three conjuncts </title>
(-> (/\ ph (/\ ps (/\ ch th))) th)
biimpa # <title> Inference from logical equivalence </title>
(-> ph (<-> ps ch))(-> (/\ ph ps) ch)
biimpar # <title> Inference from logical equivalence </title>
(-> ph (<-> ps ch))(-> (/\ ph ch) ps)
biimpac # <title> Inference from logical equivalence </title>
(-> ph (<-> ps ch))(-> (/\ ps ph) ch)
biimparc # <title> Inference from logical equivalence </title>
(-> ph (<-> ps ch))(-> (/\ ch ph) ps)
pm3.26bda # <title> Deduction eliminating a conjunct </title>
(-> ph (<-> ps (/\ ch th)))(-> (/\ ph ps) ch)
pm3.27bda # <title> Deduction eliminating a conjunct </title>
(-> ph (<-> ps (/\ ch th)))(-> (/\ ph ps) th)
jaob Disjunction of antecedents. Compare Theorem *4.77 of [bib/WhiteheadRussell] p. 121. # <title> Distributive Property </title> # <suggest> left('Distribute', '→') right('Distribute', '∧') </suggest>
(<-> (-> (\/ ph ch) ps) (/\ (-> ph ps) (-> ch ps)))
pm4.77 Theorem *4.77 of [bib/WhiteheadRussell] p. 121. # <title> Distributive Property </title> # <suggest> right('Distribute', '∧') left('Distribute', '→') </suggest>
(<-> (/\ (-> ps ph) (-> ch ph)) (-> (\/ ps ch) ph))
jaod # <title> Join Antecedents </title>
(-> ph (-> ps ch)) , (-> ph (-> th ch))(-> ph (-> (\/ ps th) ch))
jaoian # <title> Join Antecedents </title>
(-> (/\ ph ps) ch) , (-> (/\ th ps) ch)(-> (/\ (\/ ph th) ps) ch)
jaodan Deduction disjoining the antecedents of two implications. # <title> Join Antecedents </title>
(-> (/\ ph ps) ch) , (-> (/\ ph th) ch)(-> (/\ ph (\/ ps th)) ch)
jaao Inference conjoining and disjoining the antecedents of two implications.
(-> ph (-> ps ch)) , (-> th (-> ta ch))(-> (/\ ph th) (-> (\/ ps ta) ch))
jaoa Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.) # <title> Join Antecedents </title>
(-> ph (-> ps ch)) , (-> th (-> ta ch))(-> (\/ ph th) (-> (/\ ps ta) ch))
pm2.63 Theorem *2.63 of [bib/WhiteheadRussell] p. 107.
(-> (\/ ph ps) (-> (\/ (-. ph) ps) ps))
pm2.64 Theorem *2.64 of [bib/WhiteheadRussell] p. 107.
(-> (\/ ph ps) (-> (\/ ph (-. ps)) ph))
pm3.44 Theorem *3.44 of [bib/WhiteheadRussell] p. 113.
(-> (/\ (-> ps ph) (-> ch ph)) (-> (\/ ps ch) ph))
pm4.43 Theorem *4.43 of [bib/WhiteheadRussell] p. 119. # <title> Excluded Middle </title> # <suggest> left('Simplify', '∧') </suggest>
(<-> ph (/\ (\/ ph ps) (\/ ph (-. ps))))
anidm # <title> Conjunction is Idempotent </title> # <suggest> right('Simplify', '∧') </suggest>
(<-> (/\ ph ph) ph)
pm4.24 Theorem *4.24 of [bib/WhiteheadRussell] p. 117. # <title> Conjunction is Idempotent </title>
(<-> ph (/\ ph ph))
anidms # <title> Conjunction is Idempotent </title> # <table> # (-> (/\ <r> ph [ <r> ph ) ps) # (-> [ <r> ph ps) # </table>
(-> (/\ ph ph) ps)(-> ph ps)
anidmdbi # <title> Conjunction is Idempotent </title>
(<-> (-> ph (/\ ps ps)) (-> ph ps))
ancom # <title> Commute Conjunction </title> # <suggest> right('Commute', '∧') </suggest>
(<-> (/\ ph ps) (/\ ps ph))
ancomd Commutation of conjuncts in consequent. (Contributed by Jeff Hankins, 14-Aug-2009.) # <title> Commute Conjunction </title>
(-> ph (/\ ps ch))(-> ph (/\ ch ps))
ancoms Inference commuting conjunction in antecedent. //Notational convention//: We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism ([[syl]]) -type inference in a proof. # <title> Commute Conjunction </title>
(-> (/\ ph ps) ch)(-> (/\ ps ph) ch)
ancomsd Deduction commuting conjunction in antecedent. # <title> Commute Conjunction </title>
(-> ph (-> (/\ ps ch) th))(-> ph (-> (/\ ch ps) th))
pm3.22 Theorem *3.22 of [bib/WhiteheadRussell] p. 111. # <title> Commute Conjunction </title>
(-> (/\ ph ps) (/\ ps ph))
anass Associative law for conjunction. Theorem *4.32 of [bib/WhiteheadRussell] p. 118. # <title> Associative Property </title> # <suggest> right('Associate', 'R') left('Associate', 'L') </suggest>
(<-> (/\ (/\ ph ps) ch) (/\ ph (/\ ps ch)))
anasss Associative law for conjunction applied to antecedent (eliminates syllogism). # <title> Associative Property </title>
(-> (/\ (/\ ph ps) ch) th)(-> (/\ ph (/\ ps ch)) th)
anassrs Associative law for conjunction applied to antecedent (eliminates syllogism). # <title> Associative Property </title>
(-> (/\ ph (/\ ps ch)) th)(-> (/\ (/\ ph ps) ch) th)
imdistan Distribution of implication with conjunction. # <title> Distributive Property </title>
(<-> (-> ph (-> ps ch)) (-> (/\ ph ps) (/\ ph ch)))
imdistani Distribution of implication with conjunction. # <title> Distributive Property </title>
(-> ph (-> ps ch))(-> (/\ ph ps) (/\ ph ch))
imdistanri Distribution of implication with conjunction. # <title> Distributive Property </title>
(-> ph (-> ps ch))(-> (/\ ps ph) (/\ ch ph))
imdistand Distribution of implication with conjunction (deduction rule). # <title> Distributive Property </title>
(-> ph (-> ps (-> ch th)))(-> ph (-> (/\ ps ch) (/\ ps th)))
pm5.3 Theorem *5.3 of [bib/WhiteheadRussell] p. 125. # <title> Distributive Property </title>
(<-> (-> (/\ ph ps) ch) (-> (/\ ph ps) (/\ ph ch)))
pm5.61 Theorem *5.61 of [bib/WhiteheadRussell] p. 125. # <title> Eliminate Disjoint </title>
(<-> (/\ (\/ ph ps) (-. ps)) (/\ ph (-. ps)))
sylan # <title> Syllogism </title>
(-> (/\ ph ps) ch) , (-> th ph)(-> (/\ th ps) ch)
sylanb # <title> Syllogism </title>
(-> (/\ ph ps) ch) , (<-> th ph)(-> (/\ th ps) ch)
sylanbr # <title> Syllogism </title>
(-> (/\ ph ps) ch) , (<-> ph th)(-> (/\ th ps) ch)
sylan2 # <title> Syllogism </title>
(-> (/\ ph ps) ch) , (-> th ps)(-> (/\ ph th) ch)
sylan2b # <title> Syllogism </title>
(-> (/\ ph ps) ch) , (<-> th ps)(-> (/\ ph th) ch)
sylan2br # <title> Syllogism </title>
(-> (/\ ph ps) ch) , (<-> ps th)(-> (/\ ph th) ch)
syl2an # <title> Double Syllogism </title>
(-> (/\ ph ps) ch) , (-> th ph) , (-> ta ps)(-> (/\ th ta) ch)
syl2anb # <title> Double Syllogism </title>
(-> (/\ ph ps) ch) , (<-> th ph) , (<-> ta ps)(-> (/\ th ta) ch)
syl2anbr # <title> Double Syllogism </title>
(-> (/\ ph ps) ch) , (<-> ph th) , (<-> ps ta)(-> (/\ th ta) ch)
syland # <title> Syllogism </title>
(-> ph (-> (/\ ps ch) th)) , (-> ph (-> ta ps))(-> ph (-> (/\ ta ch) th))
sylan2d # <title> Syllogism </title>
(-> ph (-> (/\ ps ch) th)) , (-> ph (-> ta ch))(-> ph (-> (/\ ps ta) th))
syl2and # <title> Syllogism </title>
(-> ph (-> (/\ ps ch) th)) , (-> ph (-> ta ps)) , (-> ph (-> et ch))(-> ph (-> (/\ ta et) th))
sylanl1 # <title> Syllogism </title>
(-> (/\ (/\ ph ps) ch) th) , (-> ta ph)(-> (/\ (/\ ta ps) ch) th)
sylanl2 # <title> Syllogism </title>
(-> (/\ (/\ ph ps) ch) th) , (-> ta ps)(-> (/\ (/\ ph ta) ch) th)
sylanr1 # <title> Syllogism </title>
(-> (/\ ph (/\ ps ch)) th) , (-> ta ps)(-> (/\ ph (/\ ta ch)) th)
sylanr2 # <title> Syllogism </title>
(-> (/\ ph (/\ ps ch)) th) , (-> ta ch)(-> (/\ ph (/\ ps ta)) th)
sylani # <title> Syllogism </title>
(-> ph (-> (/\ ps ch) th)) , (-> ta ps)(-> ph (-> (/\ ta ch) th))
sylan2i # <title> Syllogism </title>
(-> ph (-> (/\ ps ch) th)) , (-> ta ch)(-> ph (-> (/\ ps ta) th))
syl2ani # <title> Syllogism </title>
(-> ph (-> (/\ ps ch) th)) , (-> ta ps) , (-> et ch)(-> ph (-> (/\ ta et) th))
syldan A syllogism deduction with conjoined antecents. # <title> Syllogism </title>
(-> (/\ ph ps) ch) , (-> (/\ ph ch) th)(-> (/\ ph ps) th)
sylan9 Nested syllogism inference conjoining dissimilar antecedents. # <title> Syllogism </title>
(-> ph (-> ps ch)) , (-> th (-> ch ta))(-> (/\ ph th) (-> ps ta))
sylan9r Nested syllogism inference conjoining dissimilar antecedents. # <title> Syllogism </title>
(-> ph (-> ps ch)) , (-> th (-> ch ta))(-> (/\ th ph) (-> ps ta))
mpan9 Modus ponens conjoining dissimilar antecedents. # <title> Modus Ponens </title>
(-> ph ps) , (-> ch (-> ps th))(-> (/\ ph ch) th)
sylanc A syllogism inference combined with contraction. # <title> Syllogism & Contraction </title>
(-> (/\ ph ps) ch) , (-> th ph) , (-> th ps)(-> th ch)
sylancl # <title> Syllogism </title>
(-> (/\ ph ps) ch) , (-> th ph) , ps(-> th ch)
sylancr # <title> Syllogism </title>
(-> (/\ ph ps) ch) , ph , (-> th ps)(-> th ch)
syl2anc # <title> Syllogism & Contraction </title>
(-> (/\ (/\ ph ps) (/\ ch th)) ta) , (-> et ph) , (-> et ps) , (-> et ch) , (-> et th)(-> et ta)
sylancb # <title> Syllogism & Contraction </title>
(-> (/\ ph ps) ch) , (<-> th ph) , (<-> th ps)(-> th ch)
sylancbr # <title> Syllogism & Contraction </title>
(-> (/\ ph ps) ch) , (<-> ph th) , (<-> ps th)(-> th ch)
sylancom # <title> Syllogism & Commute </title>
(-> (/\ ph ps) ch) , (-> (/\ ch ps) th)(-> (/\ ph ps) th)
pm2.61ian # <title> Eliminate Antecedent by Cases </title>
(-> (/\ ph ps) ch) , (-> (/\ (-. ph) ps) ch)(-> ps ch)
pm2.61dan # <title> Eliminate Antecedent by Cases </title>
(-> (/\ ph ps) ch) , (-> (/\ ph (-. ps)) ch)(-> ph ch)
condan # <title> Proof by contradiction </title>
(-> (/\ ph (-. ps)) ch) , (-> (/\ ph (-. ps)) (-. ch))(-> ph ps)
abai # <title> Introduce conjunct as antecedent </title> # <suggest> left('Simplify', '→') </suggest>
(<-> (/\ ph ps) (/\ ph (-> ph ps)))
anbi2i # <title> Add conjunct to both sides </title> # <summary> Introduce a left conjunct to both sides of a logical equivalence. </summary> # <table> # (<-> [ ph ] [ [ ps) # (<-> (/\ ch [ ph ] ) [ (/\ ch [ ps)) # </table>
(<-> ph ps)(<-> (/\ ch ph) (/\ ch ps))
anbi1i # <title> Add conjunct to both sides </title> # <summary> Introduce a right conjunct to both sides of a logical equivalence. </summary> # <table> # (<-> ph ] ] [ ps ] ) # (<-> (/\ ph ] ch) ] (/\ [ ps ] ch)) # </table>
(<-> ph ps)(<-> (/\ ph ch) (/\ ps ch))
anbi12i # <title> Conjoin both sides of two equivalences </title> # <table> # (<-> ph ] ] ] [ ps ] ] ) # (<-> [ [ ch ] [ [ th ] ) # (<-> (/\ ph ] [ ch ] ) (/\ [ ps [ th ] )) # </table>
(<-> ph ps) , (<-> ch th)(<-> (/\ ph ch) (/\ ps th))
pm5.53 Theorem *5.53 of [bib/WhiteheadRussell] p. 125.
(<-> (-> (\/ (\/ ph ps) ch) th) (/\ (/\ (-> ph th) (-> ps th)) (-> ch th)))
an12 # <title> Rearrangement conjunction </title>
(<-> (/\ ph (/\ ps ch)) (/\ ps (/\ ph ch)))
an23 # <title> Rearrangement conjunction </title>
(<-> (/\ (/\ ph ps) ch) (/\ (/\ ph ch) ps))
an1s # <title> Rearrangement conjunction </title>
(-> (/\ ph (/\ ps ch)) th)(-> (/\ ps (/\ ph ch)) th)
ancom2s # <title> Rearrangement conjunction </title>
(-> (/\ ph (/\ ps ch)) th)(-> (/\ ph (/\ ch ps)) th)
ancom13s Deduction rearranging conjuncts. # <title> Rearrangement conjunction </title>
(-> (/\ ph (/\ ps ch)) th)(-> (/\ ch (/\ ps ph)) th)
an1rs Deduction rearranging conjuncts. # <title> Rearrangement conjunction </title>
(-> (/\ (/\ ph ps) ch) th)(-> (/\ (/\ ph ch) ps) th)
ancom1s Inference commuting a nested conjunction in antecedent. # <title> Rearrangement conjunction </title>
(-> (/\ (/\ ph ps) ch) th)(-> (/\ (/\ ps ph) ch) th)
ancom31s Deduction rearranging conjuncts. # <title> Rearrangement conjunction </title>
(-> (/\ (/\ ph ps) ch) th)(-> (/\ (/\ ch ps) ph) th)
anabs1 # <title> Absorb conjunct </title>
(<-> (/\ (/\ ph ps) ph) (/\ ph ps))
anabs5 # <title> Absorb conjunct </title>
(<-> (/\ ph (/\ ph ps)) (/\ ph ps))
anabs7 # <title> Absorb conjunct </title>
(<-> (/\ ps (/\ ph ps)) (/\ ph ps))
anabsi5 # <title> Absorb conjunct </title>
(-> ph (-> (/\ ph ps) ch))(-> (/\ ph ps) ch)
anabsi6 # <title> Absorb conjunct </title>
(-> ph (-> (/\ ps ph) ch))(-> (/\ ph ps) ch)
anabsi7 # <title> Absorb antecedent into conjunction </title>
(-> ps (-> (/\ ph ps) ch))(-> (/\ ph ps) ch)
anabsi8 # <title> Absorb antecedent into conjunction </title>
(-> ps (-> (/\ ps ph) ch))(-> (/\ ph ps) ch)
anabss1 # <title> Absorb antecedent into conjunction </title>
(-> (/\ (/\ ph ps) ph) ch)(-> (/\ ph ps) ch)
anabss3 # <title> Absorb antecedent into conjunction </title>
(-> (/\ (/\ ph ps) ps) ch)(-> (/\ ph ps) ch)
anabss4 # <title> Absorb antecedent into conjunction </title>
(-> (/\ (/\ ps ph) ps) ch)(-> (/\ ph ps) ch)
anabss5 # <title> Absorb antecedent into conjunction </title>
(-> (/\ ph (/\ ph ps)) ch)(-> (/\ ph ps) ch)
anabss7 # <title> Absorb antecedent into conjunction </title>
(-> (/\ ps (/\ ph ps)) ch)(-> (/\ ph ps) ch)
anabsan # <title> Absorb antecedent into conjunction </title>
(-> (/\ (/\ ph ph) ps) ch)(-> (/\ ph ps) ch)
anabsan2 # <title> Absorb antecedent into conjunction </title>
(-> (/\ ph (/\ ps ps)) ch)(-> (/\ ph ps) ch)
an4 # <title> Rearrange Conjunction </title>
(<-> (/\ (/\ ph ps) (/\ ch th)) (/\ (/\ ph ch) (/\ ps th)))
an42 # <title> Rearrange Conjunction </title>
(<-> (/\ (/\ ph ps) (/\ ch th)) (/\ (/\ ph ch) (/\ th ps)))
an4s # <title> Rearrange Conjunction </title>
(-> (/\ (/\ ph ps) (/\ ch th)) ta)(-> (/\ (/\ ph ch) (/\ ps th)) ta)
an42s # <title> Rearrange Conjunction </title>
(-> (/\ (/\ ph ps) (/\ ch th)) ta)(-> (/\ (/\ ph ch) (/\ th ps)) ta)
anandi Distribution of conjunction over conjunction. # <title> Distributive Property </title>
(<-> (/\ ph (/\ ps ch)) (/\ (/\ ph ps) (/\ ph ch)))
anandir Distribution of conjunction over conjunction. # <title> Distributive Property </title>
(<-> (/\ (/\ ph ps) ch) (/\ (/\ ph ch) (/\ ps ch)))
anandis Inference that undistributes conjunction in the antecedent. # <title> Distributive Property </title>
(-> (/\ (/\ ph ps) (/\ ph ch)) ta)(-> (/\ ph (/\ ps ch)) ta)
anandirs Inference that undistributes conjunction in the antecedent. # <title> Distributive Property </title>
(-> (/\ (/\ ph ch) (/\ ps ch)) ta)(-> (/\ (/\ ph ps) ch) ta)
dfbi2 A theorem similar to the standard definition of the biconditional. Definition of [bib/Margaris] p. 49. # <title> Definition of biconditional </title> # <summary> # See <a href="def-bi">def-bi</a> for more information. # </summary> # <suggest> left('Simplify', '↔') </suggest>
(<-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph)))
dfbi # <title> Definition of biconditional </title> # <summary> # Definition [[df-bi]] rewritten in an abbreviated form to help intuitive # understanding of that definition. Note that it is a conjunction of # two implications; one which asserts properties that follow from the # biconditional and one which asserts properties that imply the # biconditional. # </summary>
(/\ (-> (<-> ph ps) (/\ (-> ph ps) (-> ps ph))) (-> (/\ (-> ph ps) (-> ps ph)) (<-> ph ps)))
impbid Deduce an equivalence from two implications. # <title> Deduce Biconditional from two conditionals </title> # <table> # (-> ph (-> [ <r> ps <g> ch ] )) # (-> ph (-> [ <g> ch <r> ps ] )) # (-> ph (<-> [ <r> ps <g> ch ] )) # </table>
(-> ph (-> ps ch)) , (-> ph (-> ch ps))(-> ph (<-> ps ch))
impbid1 # <title> Infer Biconditional from two conditionals </title>
(-> ph (-> ps ch)) , (-> ch ps)(-> ph (<-> ps ch))
impbid2 # <title> Infer Biconditional from two conditionals </title>
(-> ps ch) , (-> ph (-> ch ps))(-> ph (<-> ps ch))
impbida Deduce an equivalence from two implications. # <title> Deduce Biconditional from two conditionals </title>
(-> (/\ ph ps) ch) , (-> (/\ ph ch) ps)(-> ph (<-> ps ch))
bicom Commutative law for equivalence. Theorem *4.21 of [bib/WhiteheadRussell] p. 117. # <title> Commutative Biconditional </title>
(<-> (<-> ph ps) (<-> ps ph))
bicomd Commute two sides of a biconditional in a deduction. # <title> Commutative Biconditional </title>
(-> ph (<-> ps ch))(-> ph (<-> ch ps))
notbi Contraposition. Theorem *4.11 of [bib/WhiteheadRussell] p. 117. # <title> Negate Both Sides </title> # <suggest> left('Simplify', '¬') right('Add', '¬') </suggest>
(<-> (<-> ph ps) (<-> (-. ph) (-. ps)))
con4bii # <title> Contraposition </title>
(<-> (-. ph) (-. ps))(<-> ph ps)
con4bid # <title> Contraposition </title>
(-> ph (<-> (-. ps) (-. ch)))(-> ph (<-> ps ch))
con2bi Contraposition. Theorem *4.12 of [bib/WhiteheadRussell] p. 117. # <title> Contraposition </title>
(<-> (<-> ph (-. ps)) (<-> ps (-. ph)))
con2bid # <title> Contraposition </title>
(-> ph (<-> ps (-. ch)))(-> ph (<-> ch (-. ps)))
con1bid # <title> Contraposition </title>
(-> ph (<-> (-. ps) ch))(-> ph (<-> (-. ch) ps))
bitrd Deduction form of [[bitri]]. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (-> ph (<-> ch th))(-> ph (<-> ps th))
bitr2d Deduction form of [[bitr2i]]. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (-> ph (<-> ch th))(-> ph (<-> th ps))
bitr3d Deduction form of [[bitr3i]]. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (-> ph (<-> ps th))(-> ph (<-> ch th))
bitr4d Deduction form of [[bitr4i]]. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (-> ph (<-> th ch))(-> ph (<-> ps th))
syl5bb A syllogism inference from two biconditionals. # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (<-> th ps)(-> ph (<-> th ch))
syl5rbb A syllogism inference from two biconditionals. # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (<-> th ps)(-> ph (<-> ch th))
syl5bbr A syllogism inference from two biconditionals. # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (<-> ps th)(-> ph (<-> th ch))
syl5rbbr A syllogism inference from two biconditionals. # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (<-> ps th)(-> ph (<-> ch th))
syl6bb A syllogism inference from two biconditionals. # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (<-> ch th)(-> ph (<-> ps th))
syl6rbb A syllogism inference from two biconditionals. # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (<-> ch th)(-> ph (<-> th ps))
syl6bbr A syllogism inference from two biconditionals. # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (<-> th ch)(-> ph (<-> ps th))
syl6rbbr A syllogism inference from two biconditionals. # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (<-> th ch)(-> ph (<-> th ps))
sylan9bb Nested syllogism inference conjoining dissimilar antecedents. # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (-> th (<-> ch ta))(-> (/\ ph th) (<-> ps ta))
sylan9bbr Nested syllogism inference conjoining dissimilar antecedents. # <title> Syllogism </title>
(-> ph (<-> ps ch)) , (-> th (<-> ch ta))(-> (/\ th ph) (<-> ps ta))
3imtr3d More general version of [[3imtr3i]]. Useful for converting conditional definitions in a formula. # <title> Syllogism </title>
(-> ph (-> ps ch)) , (-> ph (<-> ps th)) , (-> ph (<-> ch ta))(-> ph (-> th ta))
3imtr4d More general version of [[3imtr4i]]. Useful for converting conditional definitions in a formula. # <title> Syllogism </title>
(-> ph (-> ps ch)) , (-> ph (<-> th ps)) , (-> ph (<-> ta ch))(-> ph (-> th ta))
3bitrd Deduction from transitivity of biconditional. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (-> ph (<-> ch th)) , (-> ph (<-> th ta))(-> ph (<-> ps ta))
3bitrrd Deduction from transitivity of biconditional. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (-> ph (<-> ch th)) , (-> ph (<-> th ta))(-> ph (<-> ta ps))
3bitr2d Deduction from transitivity of biconditional. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (-> ph (<-> th ch)) , (-> ph (<-> th ta))(-> ph (<-> ps ta))
3bitr2rd Deduction from transitivity of biconditional. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (-> ph (<-> th ch)) , (-> ph (<-> th ta))(-> ph (<-> ta ps))
3bitr3d Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (-> ph (<-> ps th)) , (-> ph (<-> ch ta))(-> ph (<-> th ta))
3bitr3rd Deduction from transitivity of biconditional. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (-> ph (<-> ps th)) , (-> ph (<-> ch ta))(-> ph (<-> ta th))
3bitr4d Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (-> ph (<-> th ps)) , (-> ph (<-> ta ch))(-> ph (<-> th ta))
3bitr4rd Deduction from transitivity of biconditional. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (-> ph (<-> th ps)) , (-> ph (<-> ta ch))(-> ph (<-> ta th))
3imtr3g More general version of [[3imtr3i]]. Useful for converting definitions in a formula. # <title> Syllogism </title>
(-> ph (-> ps ch)) , (<-> ps th) , (<-> ch ta)(-> ph (-> th ta))
3imtr4g More general version of [[3imtr4i]]. Useful for converting definitions in a formula. # <title> Syllogism </title>
(-> ph (-> ps ch)) , (<-> th ps) , (<-> ta ch)(-> ph (-> th ta))
3bitr3g More general version of [[3bitr3i]]. Useful for converting definitions in a formula. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (<-> ps th) , (<-> ch ta)(-> ph (<-> th ta))
3bitr4g More general version of [[3bitr4i]]. Useful for converting definitions in a formula. # <title> Transitive Property </title>
(-> ph (<-> ps ch)) , (<-> th ps) , (<-> ta ch)(-> ph (<-> th ta))
prth Theorem *3.47 of [bib/WhiteheadRussell] p. 113. # <title> Praeclarum Theorema </title> # <suggest> right('Infer', '→') </suggest> # <summary> # This was proved by Leibniz, and it evidently pleased him enough to call it # 'praeclarum theorema' (splendid theorem). # </summary>
(-> (/\ (-> ph ps) (-> ch th)) (-> (/\ ph ch) (/\ ps th)))
pm3.48 Theorem *3.48 of [bib/WhiteheadRussell] p. 114.
(-> (/\ (-> ph ps) (-> ch th)) (-> (\/ ph ch) (\/ ps th)))
anim12d Conjoin antecedents and consequents in a deduction. # <title> Join antecedents and consequents </title>
(-> ph (-> ps ch)) , (-> ph (-> th ta))(-> ph (-> (/\ ps th) (/\ ch ta)))
anim12ii Conjoin antecedents and consequents in a deduction. # <title> Join antecedents and consequents </title>
(-> ph (-> ps ch)) , (-> th (-> ps ta))(-> (/\ ph th) (-> ps (/\ ch ta)))
anim1d Add a conjunct to right of antecedent and consequent in a deduction. # <title> Add a conjunct to antecedent and consequent </title>
(-> ph (-> ps ch))(-> ph (-> (/\ ps th) (/\ ch th)))
anim2d Add a conjunct to left of antecedent and consequent in a deduction. # <title> Add a conjunct to antecedent and consequent </title>
(-> ph (-> ps ch))(-> ph (-> (/\ th ps) (/\ th ch)))
pm3.45 Theorem *3.45 (Fact) of [bib/WhiteheadRussell] p. 113.
(-> (-> ph ps) (-> (/\ ph ch) (/\ ps ch)))
im2anan9 Deduction joining nested implications to form implication of conjunctions. # <title> Join nested implications </title>
(-> ph (-> ps ch)) , (-> th (-> ta et))(-> (/\ ph th) (-> (/\ ps ta) (/\ ch et)))
im2anan9r Deduction joining nested implications to form implication of conjunctions. # <title> Join nested implications </title>
(-> ph (-> ps ch)) , (-> th (-> ta et))(-> (/\ th ph) (-> (/\ ps ta) (/\ ch et)))
orim12d Disjoin antecedents and consequents in a deduction. # <title> Join antecedents and consequents </title>
(-> ph (-> ps ch)) , (-> ph (-> th ta))(-> ph (-> (\/ ps th) (\/ ch ta)))
orim1d Disjoin antecedents and consequents in a deduction. # <title> Add disjunct to antecedent and consequent </title>
(-> ph (-> ps ch))(-> ph (-> (\/ ps th) (\/ ch th)))
orim2d Disjoin antecedents and consequents in a deduction. # <title> Add disjunct to antecedent and consequent </title>
(-> ph (-> ps ch))(-> ph (-> (\/ th ps) (\/ th ch)))
orim2 Axiom *1.6 (Sum) of [bib/WhiteheadRussell] p. 97. # <title> Add disjunct to antecedent and consequent </title>
(-> (-> ps ch) (-> (\/ ph ps) (\/ ph ch)))
pm2.38 Theorem *2.38 of [bib/WhiteheadRussell] p. 105. # <title> Add disjunct to antecedent and consequent </title>
(-> (-> ps ch) (-> (\/ ps ph) (\/ ch ph)))
pm2.36 Theorem *2.36 of [bib/WhiteheadRussell] p. 105. # <title> Add disjunct to antecedent and consequent </title>
(-> (-> ps ch) (-> (\/ ph ps) (\/ ch ph)))
pm2.37 Theorem *2.37 of [bib/WhiteheadRussell] p. 105. # <title> Add disjunct to antecedent and consequent </title>
(-> (-> ps ch) (-> (\/ ps ph) (\/ ph ch)))
pm2.73 Theorem *2.73 of [bib/WhiteheadRussell] p. 108.
(-> (-> ph ps) (-> (\/ (\/ ph ps) ch) (\/ ps ch)))
pm2.74 Theorem *2.74 of [bib/WhiteheadRussell] p. 108.
(-> (-> ps ph) (-> (\/ (\/ ph ps) ch) (\/ ph ch)))
pm2.75 Theorem *2.75 of [bib/WhiteheadRussell] p. 108.
(-> (\/ ph ps) (-> (\/ ph (-> ps ch)) (\/ ph ch)))
pm2.76 Theorem *2.76 of [bib/WhiteheadRussell] p. 108.
(-> (\/ ph (-> ps ch)) (-> (\/ ph ps) (\/ ph ch)))
pm2.8 Theorem *2.8 of [bib/WhiteheadRussell] p. 108.
(-> (\/ ps ch) (-> (\/ (-. ch) th) (\/ ps th)))
pm2.81 Theorem *2.81 of [bib/WhiteheadRussell] p. 108.
(-> (-> ps (-> ch th)) (-> (\/ ph ps) (-> (\/ ph ch) (\/ ph th))))
pm2.82 Theorem *2.82 of [bib/WhiteheadRussell] p. 108.
(-> (\/ (\/ ph ps) ch) (-> (\/ (\/ ph (-. ch)) th) (\/ (\/ ph ps) th)))
pm2.85 Theorem *2.85 of [bib/WhiteheadRussell] p. 108.
(-> (-> (\/ ph ps) (\/ ph ch)) (\/ ph (-> ps ch)))
pm3.2ni # <title> Disjunction of negated premises </title>
(-. ph) , (-. ps)(-. (\/ ph ps))
orabs Absorption of redundant internal disjunct. Compare Theorem *4.45 of [bib/WhiteheadRussell] p. 119. # <title> Absorb redundant disjunct </title>
(<-> ph (/\ (\/ ph ps) ph))
oranabs Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton 23-Jun-2005.) # <title> Absorb redundant disjunct </title>
(<-> (/\ (\/ ph (-. ps)) ps) (/\ ph ps))
pm5.74 Distribution of implication over biconditional. Theorem *5.74 of [bib/WhiteheadRussell] p. 126. # <title> Distributive Property </title>
(<-> (-> ph (<-> ps ch)) (<-> (-> ph ps) (-> ph ch)))
pm5.74i Distribution of implication over biconditional (inference rule). # <title> Distributive Property </title>
(-> ph (<-> ps ch))(<-> (-> ph ps) (-> ph ch))
pm5.74d Distribution of implication over biconditional (deduction rule). # <title> Distributive Property </title>
(-> ph (-> ps (<-> ch th)))(-> ph (<-> (-> ps ch) (-> ps th)))
pm5.74da Distribution of implication over biconditional (deduction rule). # <title> Distributive Property </title>
(-> (/\ ph ps) (<-> ch th))(-> ph (<-> (-> ps ch) (-> ps th)))
pm5.74ri Distribution of implication over biconditional (reverse inference rule). # <title> Distributive Property </title>
(<-> (-> ph ps) (-> ph ch))(-> ph (<-> ps ch))
pm5.74rd Distribution of implication over biconditional (deduction rule). # <title> Distributive Property </title>
(-> ph (<-> (-> ps ch) (-> ps th)))(-> ph (-> ps (<-> ch th)))
mpbidi A deduction from a biconditional, related to modus ponens. # <title> Modus Ponens </title>
(-> th (-> ph ps)) , (-> ph (<-> ps ch))(-> th (-> ph ch))
ibib Implication in terms of implication and biconditional. # <title> Implication & Biconditional </title> # <suggest> left('Simplify', '↔') </suggest>
(<-> (-> ph ps) (-> ph (<-> ph ps)))
ibibr Implication in terms of implication and biconditional. # <title> Implication & Biconditional </title> # <suggest> left('Simplify', '↔') </suggest>
(<-> (-> ph ps) (-> ph (<-> ps ph)))
ibi # <title> Biconditional to Condition <title> # <summary> # Inference that converts a biconditional implied by one of its arguments, # into an implication. # </summary>
(-> ph (<-> ph ps))(-> ph ps)
ibir # <title> Biconditional to Condition <title> # <summary> # Inference that converts a biconditional implied by one of its arguments, # into an implication. # </summary>
(-> ph (<-> ps ph))(-> ph ps)
ibd # <title> Biconditional to Condition <title> # <summary> # Deduction that converts a biconditional implied by one of its arguments, # into an implication. # </summary>
(-> ph (-> ps (<-> ps ch)))(-> ph (-> ps ch))
pm5.501 Theorem *5.501 of [bib/WhiteheadRussell] p. 125.
(-> ph (<-> ps (<-> ph ps)))
ordi Distributive law for disjunction. Theorem *4.41 of [bib/WhiteheadRussell] p. 119. # <title> Distributive Property </title> # <suggest> right('Distribute', 'L') left('Distribute', '-L') </suggest>
(<-> (\/ ph (/\ ps ch)) (/\ (\/ ph ps) (\/ ph ch)))
ordir # <title> Distributive Property </title> # <suggest> right('Distribute', 'R') left('Distribute', '-R') </suggest>
(<-> (\/ (/\ ph ps) ch) (/\ (\/ ph ch) (\/ ps ch)))
jcab Distributive law for implication over conjunction. Compare Theorem *4.76 of [bib/WhiteheadRussell] p. 121. # <title> Distributive Property </title> # <suggest> left('Distribute', '-∧') right('Distribute', '→') </suggest>
(<-> (-> ph (/\ ps ch)) (/\ (-> ph ps) (-> ph ch)))
pm4.76 Theorem *4.76 of [bib/WhiteheadRussell] p. 121. # <title> Join antecedents </title>
(<-> (/\ (-> ph ps) (-> ph ch)) (-> ph (/\ ps ch)))
jcad Deduction conjoining the consequents of two implications. # <title> Join two implications </title>
(-> ph (-> ps ch)) , (-> ph (-> ps th))(-> ph (-> ps (/\ ch th)))
jctild Deduction conjoining a theorem to left of consequent in an implication.
(-> ph (-> ps ch)) , (-> ph th)(-> ph (-> ps (/\ th ch)))
jctird Deduction conjoining a theorem to right of consequent in an implication.
(-> ph (-> ps ch)) , (-> ph th)(-> ph (-> ps (/\ ch th)))
pm3.43 Theorem *3.43 (Comp) of [bib/WhiteheadRussell] p. 113.
(-> (/\ (-> ph ps) (-> ph ch)) (-> ph (/\ ps ch)))
andi Distributive law for conjunction. Theorem *4.4 of [bib/WhiteheadRussell] p. 118. # <title> Distributive Property </title> # <suggest> right('Distribute', 'L') left('Distribute', '-L') </suggest>
(<-> (/\ ph (\/ ps ch)) (\/ (/\ ph ps) (/\ ph ch)))
andir Distributive law for conjunction. # <title> Distributive Property </title> # <suggest> right('Distribute', 'R') left('Distribute', '-R') </suggest>
(<-> (/\ (\/ ph ps) ch) (\/ (/\ ph ch) (/\ ps ch)))
orddi Double distributive law for disjunction. # <title> Double Distributive Property </title>
(<-> (\/ (/\ ph ps) (/\ ch th)) (/\ (/\ (\/ ph ch) (\/ ph th)) (/\ (\/ ps ch) (\/ ps th))))
anddi Double distributive law for conjunction. # <title> Double Distributive Property </title>
(<-> (/\ (\/ ph ps) (\/ ch th)) (\/ (\/ (/\ ph ch) (/\ ph th)) (\/ (/\ ps ch) (/\ ps th))))
bibi2i Inference adding a biconditional to the left in an equivalence. # <title> Add biconditional to both sides of a equivalence </title> # <table> # (<-> [ ph ] [ [ ps) # (<-> (-> ch [ ph ] ) [ (-> ch [ ps)) # </table>
(<-> ph ps)(<-> (<-> ch ph) (<-> ch ps))
bibi1i Inference adding a biconditional to the right in an equivalence. # <title> Add biconditional to both sides of a equivalence </title> # <table> # (<-> ph ] ] [ ps ] ) # (<-> (<-> ph ] ch) ] (<-> [ ps ] ch)) # </table>
(<-> ph ps)(<-> (<-> ph ch) (<-> ps ch))
bibi12i The equivalence of two equivalences. # <title> Combine Two equivalences </title>
(<-> ph ps) , (<-> ch th)(<-> (<-> ph ch) (<-> ps th))
notbid Deduction negating both sides of a logical equivalence. # <title> Negate Both Sides </title>
(-> ph (<-> ps ch))(-> ph (<-> (-. ps) (-. ch)))
imbi2d Deduction adding an antecedent to both sides of a logical equivalence. # <title> Add an antecedent to both sides </title>
(-> ph (<-> ps ch))(-> ph (<-> (-> th ps) (-> th ch)))
imbi1d Deduction adding a consequent to both sides of a logical equivalence. # <title> Add a consequent to both sides </title>
(-> ph (<-> ps ch))(-> ph (<-> (-> ps th) (-> ch th)))
orbi2d Deduction adding a left disjunct to both sides of a logical equivalence. # <title> Add a disjunct to both sides </title>
(-> ph (<-> ps ch))(-> ph (<-> (\/ th ps) (\/ th ch)))
orbi1d Deduction adding a right disjunct to both sides of a logical equivalence. # <title> Add a disjunct to both sides </title>
(-> ph (<-> ps ch))(-> ph (<-> (\/ ps th) (\/ ch th)))
anbi2d Deduction adding a left conjunct to both sides of a logical equivalence. # <title> Add a conjunct to both sides </title>
(-> ph (<-> ps ch))(-> ph (<-> (/\ th ps) (/\ th ch)))
anbi1d Deduction adding a right conjunct to both sides of a logical equivalence. # <title> Add a conjunct to both sides </title>
(-> ph (<-> ps ch))(-> ph (<-> (/\ ps th) (/\ ch th)))
bibi2d Deduction adding a biconditional to the left in an equivalence. # <title> Add a biconditional to both sides </title>
(-> ph (<-> ps ch))(-> ph (<-> (<-> th ps) (<-> th ch)))
bibi1d Deduction adding a biconditional to the right in an equivalence. # <title> Add a biconditional to both sides </title>
(-> ph (<-> ps ch))(-> ph (<-> (<-> ps th) (<-> ch th)))
orbi1 Theorem *4.37 of [bib/WhiteheadRussell] p. 118. # <title> Add a disjunct to both sides </title>
(-> (<-> ph ps) (<-> (\/ ph ch) (\/ ps ch)))
anbi1 Theorem *4.36 of [bib/WhiteheadRussell] p. 118. # <title> Add a conjunct to both sides </title>
(-> (<-> ph ps) (<-> (/\ ph ch) (/\ ps ch)))
bitr Theorem *4.22 of [bib/WhiteheadRussell] p. 117. # <title> Transitive Property </title> # <suggest> right('Transitive', '↔') </suggest>
(-> (/\ (<-> ph ps) (<-> ps ch)) (<-> ph ch))
imbi1 Theorem *4.84 of [bib/WhiteheadRussell] p. 122. # <title> Add a consequent to both sides </title>
(-> (<-> ph ps) (<-> (-> ph ch) (-> ps ch)))
imbi2 Theorem *4.85 of [bib/WhiteheadRussell] p. 122. # <title> Add an antecedent to both sides </title>
(-> (<-> ph ps) (<-> (-> ch ph) (-> ch ps)))
bibi1 Theorem *4.86 of [bib/WhiteheadRussell] p. 122. # <title> Add a biconditional to both sides </title>
(-> (<-> ph ps) (<-> (<-> ph ch) (<-> ps ch)))
imbi12d Deduction joining two equivalences to form equivalence of implications. # <title> Join two equivalences into equivalent implication </title>
(-> ph (<-> ps ch)) , (-> ph (<-> th ta))(-> ph (<-> (-> ps th) (-> ch ta)))
orbi12d Deduction joining two equivalences to form equivalence of disjunctions. # <title> Join two equivalences into equivalent disjunction </title>
(-> ph (<-> ps ch)) , (-> ph (<-> th ta))(-> ph (<-> (\/ ps th) (\/ ch ta)))
anbi12d Deduction joining two equivalences to form equivalence of conjunctions. # <title> Join two equivalences into equivalent conjunction </title> # <table> # (-> ph (<-> ps ] ] ] ch ] ] ] )) # (-> ph (<-> [ [ th ] [ [ ta ] )) # (-> ph (<-> (/\ ps ] [ th) ] (/\ ch ] [ ta ] ))) # </table>
(-> ph (<-> ps ch)) , (-> ph (<-> th ta))(-> ph (<-> (/\ ps th) (/\ ch ta)))
bibi12d Deduction joining two equivalences to form equivalence of biconditionals. # <title> Join two equivalences into equivalent biconditionals </title>
(-> ph (<-> ps ch)) , (-> ph (<-> th ta))(-> ph (<-> (<-> ps th) (<-> ch ta)))
pm4.39 Theorem *4.39 of [bib/WhiteheadRussell] p. 118. # <title> Join equivalences into equivalent disjunction </title>
(-> (/\ (<-> ph ch) (<-> ps th)) (<-> (\/ ph ps) (\/ ch th)))
pm4.38 Theorem *4.38 of [bib/WhiteheadRussell] p. 118. # <title> Join equivalences into equivalent conjunction </title>
(-> (/\ (<-> ph ch) (<-> ps th)) (<-> (/\ ph ps) (/\ ch th)))
bi2anan9 Deduction joining two equivalences to form equivalence of conjunctions. # <title> Join equivalences into equivalent conjunction </title>
(-> ph (<-> ps ch)) , (-> th (<-> ta et))(-> (/\ ph th) (<-> (/\ ps ta) (/\ ch et)))
bi2anan9r Deduction joining two equivalences to form equivalence of conjunctions. # <title> Join equivalences into equivalent conjunction </title>
(-> ph (<-> ps ch)) , (-> th (<-> ta et))(-> (/\ th ph) (<-> (/\ ps ta) (/\ ch et)))
bi2bian9 Deduction joining two biconditionals with different antecedents. # <title> Join biconditionals </title>
(-> ph (<-> ps ch)) , (-> th (<-> ta et))(-> (/\ ph th) (<-> (<-> ps ta) (<-> ch et)))
pm4.71 Implication in terms of biconditional and conjunction. Theorem *4.71 of [bib/WhiteheadRussell] p. 120. # <title> Implication as a biconditional and conjunction </title>
(<-> (-> ph ps) (<-> ph (/\ ph ps)))
pm4.71r Implication in terms of biconditional and conjunction. Theorem *4.71 of [bib/WhiteheadRussell] p. 120 (with conjunct reversed). # <title> Implication as a biconditional and conjunction </title>
(<-> (-> ph ps) (<-> ph (/\ ps ph)))
pm4.71i Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [bib/WhiteheadRussell] p. 120. # <title> Implication as a biconditional and conjunction </title>
(-> ph ps)(<-> ph (/\ ph ps))
pm4.71ri Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [bib/WhiteheadRussell] p. 120 (with conjunct reversed). # <title> Implication as a biconditional and conjunction </title>
(-> ph ps)(<-> ph (/\ ps ph))
pm4.71rd Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [bib/WhiteheadRussell] p. 120. # <title> Implication as a biconditional and conjunction </title>
(-> ph (-> ps ch))(-> ph (<-> ps (/\ ch ps)))
pm4.45 Theorem *4.45 of [bib/WhiteheadRussell] p. 119. # <title> Implication as a biconditional and conjunction </title>
(<-> ph (/\ ph (\/ ph ps)))
pm4.72 Implication in terms of biconditional and disjunction. Theorem *4.72 of [bib/WhiteheadRussell] p. 121. # <title> Implication as a biconditional and conjunction </title>
(<-> (-> ph ps) (<-> ps (\/ ph ps)))
iba Introduction of antecedent as conjunct. Theorem *4.73 of [bib/WhiteheadRussell] p. 121. # <title> Introduce antecedent as conjunct </title>
(-> ph (<-> ps (/\ ps ph)))
ibar Introduction of antecedent as conjunct. # <title> Introduce antecedent as conjunct </title>
(-> ph (<-> ps (/\ ph ps)))
pm5.32 Distribution of implication over biconditional. Theorem *5.32 of [bib/WhiteheadRussell] p. 125. # <title> Distributive Property </title> # <suggest> left('Equivalence', '↔') right('Equivalence', '↔') </suggest>
(<-> (-> ph (<-> ps ch)) (<-> (/\ ph ps) (/\ ph ch)))
pm5.32i Distribution of implication over biconditional (inference rule). # <title> Distributive Property </title>
(-> ph (<-> ps ch))(<-> (/\ ph ps) (/\ ph ch))
pm5.32ri Distribution of implication over biconditional (inference rule). # <title> Distributive Property </title>
(-> ph (<-> ps ch))(<-> (/\ ps ph) (/\ ch ph))
pm5.32d Distribution of implication over biconditional (deduction rule). # <title> Distributive Property </title>
(-> ph (-> ps (<-> ch th)))(-> ph (<-> (/\ ps ch) (/\ ps th)))
pm5.32rd Distribution of implication over biconditional (deduction rule). # <title> Distributive Property </title>
(-> ph (-> ps (<-> ch th)))(-> ph (<-> (/\ ch ps) (/\ th ps)))
pm5.32da Distribution of implication over biconditional (deduction rule). # <title> Distributive Property </title>
(-> (/\ ph ps) (<-> ch th))(-> ph (<-> (/\ ps ch) (/\ ps th)))
pm5.33 Theorem *5.33 of [bib/WhiteheadRussell] p. 125.
(<-> (/\ ph (-> ps ch)) (/\ ph (-> (/\ ph ps) ch)))
pm5.36 Theorem *5.36 of [bib/WhiteheadRussell] p. 125.
(<-> (/\ ph (<-> ph ps)) (/\ ps (<-> ph ps)))
pm5.42 Theorem *5.42 of [bib/WhiteheadRussell] p. 125.
(<-> (-> ph (-> ps ch)) (-> ph (-> ps (/\ ph ch))))
bianabs Absorb a hypothesis into the second member of a biconditional. (Contributed by FL, 15-Feb-2007.) # <title> Absorb antecedent </title>
(-> ph (<-> ps (/\ ph ch)))(-> ph (<-> ps ch))
oibabs Absorption of disjunction into equivalence. # <title> Absorb disjunction </title>
(<-> (-> (\/ ph ps) (<-> ph ps)) (<-> ph ps))
exmid # <title> Law of excluded middle </title> # <summary> # Law of excluded middle, also called the principle of tertium non datur. # It says that something is either true or not true; there are no in-between # values of truth. This is an essential distinction of our classical logic # and is not a theorem of intuitionistic logic. # </summary>
(\/ ph (-. ph))
pm2.1 Theorem *2.1 of [bib/WhiteheadRussell] p. 101. # <title> Law of excluded middle </title>
(\/ (-. ph) ph)
pm2.13 Theorem *2.13 of [bib/WhiteheadRussell] p. 101. # <title> Law of excluded middle </title>
(\/ ph (-. (-. (-. ph))))
pm3.24 Law of noncontradiction. Theorem *3.24 of [bib/WhiteheadRussell] p. 111 (who call it the "law of contradiction"). # <title> Law of Noncontradiction </title> # <suggest> full('Simplify', 'F') </suggest>
(-. (/\ ph (-. ph)))
pm2.26 Theorem *2.26 of [bib/WhiteheadRussell] p. 104.
(\/ (-. ph) (-> (-> ph ps) ps))
pm5.18 Theorem *5.18 of [bib/WhiteheadRussell] p. 124. This theorem says that logical equivalence is the same as negated "exclusive-or." # <title> Logical Equivalence is Negated Exclusive Or </title>
(<-> (<-> ph ps) (-. (<-> ph (-. ps))))
nbbn Move negation outside of biconditional. Compare Theorem *5.18 of [bib/WhiteheadRussell] p. 124. # <title> Move negation outside biconditional </title>
(<-> (<-> (-. ph) ps) (-. (<-> ph ps)))
pm5.11 Theorem *5.11 of [bib/WhiteheadRussell] p. 123.
(\/ (-> ph ps) (-> (-. ph) ps))
pm5.12 Theorem *5.12 of [bib/WhiteheadRussell] p. 123.
(\/ (-> ph ps) (-> ph (-. ps)))
pm5.13 Theorem *5.13 of [bib/WhiteheadRussell] p. 123.
(\/ (-> ph ps) (-> ps ph))
pm5.14 Theorem *5.14 of [bib/WhiteheadRussell] p. 123.
(\/ (-> ph ps) (-> ps ch))
pm5.15 Theorem *5.15 of [bib/WhiteheadRussell] p. 124.
(\/ (<-> ph ps) (<-> ph (-. ps)))
pm5.16 Theorem *5.16 of [bib/WhiteheadRussell] p. 124.
(-. (/\ (<-> ph ps) (<-> ph (-. ps))))
pm5.17 Theorem *5.17 of [bib/WhiteheadRussell] p. 124.
(<-> (/\ (\/ ph ps) (-. (/\ ph ps))) (<-> ph (-. ps)))
pm5.19 Theorem *5.19 of [bib/WhiteheadRussell] p. 124. # <title> An proposition is not equivalence to its negation </title>
(-. (<-> ph (-. ph)))
dfbi3 An alternate definition of the biconditional. Theorem *5.23 of [bib/WhiteheadRussell] p. 124. # <title> An alternative definition of biconditional </title> # <summary> # See <a href="def-bi">def-bi</a> for more information. # </summary>
(<-> (<-> ph ps) (\/ (/\ ph ps) (/\ (-. ph) (-. ps))))
xor Two ways to express "exclusive or." Theorem *5.22 of [bib/WhiteheadRussell] p. 124. # <title> Two ways to express Exclusive Or </title>
(<-> (-. (<-> ph ps)) (\/ (/\ ph (-. ps)) (/\ ps (-. ph))))
pm5.24 Theorem *5.24 of [bib/WhiteheadRussell] p. 124. # <title> Two ways to express Exclusive Or </title>
(<-> (-. (\/ (/\ ph ps) (/\ (-. ph) (-. ps)))) (\/ (/\ ph (-. ps)) (/\ ps (-. ph))))
xor2 Two ways to express "exclusive or." # <title> Two ways to express Exclusive Or </title>
(<-> (-. (<-> ph ps)) (/\ (\/ ph ps) (-. (/\ ph ps))))
xor3 Two ways to express "exclusive or." # <title> Two ways to express Exclusive Or </title>
(<-> (-. (<-> ph ps)) (<-> ph (-. ps)))
xordi Conjunction distributes over exclusive-or, using #(-. (<-> ph ps))# to express exclusive-or. This is one way to interpret the distributive law of multiplication over addition in modulo 2 arithmetic. # <title> Distributive Property </title>
(<-> (/\ ph (-. (<-> ps ch))) (-. (<-> (/\ ph ps) (/\ ph ch))))
pm5.55 Theorem *5.55 of [bib/WhiteheadRussell] p. 125.
(\/ (<-> (\/ ph ps) ph) (<-> (\/ ph ps) ps))
pm5.1 Two propositions are equivalent if they are both true. Theorem *5.1 of [bib/WhiteheadRussell] p. 123. # <title> Two truths are equivalent </title>
(-> (/\ ph ps) (<-> ph ps))
pm5.21 Two propositions are equivalent if they are both false. Theorem *5.21 of [bib/WhiteheadRussell] p. 124. # <title> Two falsehoods are equivalent </title>
(-> (/\ (-. ph) (-. ps)) (<-> ph ps))
pm5.21ni # <title> Two propositions implying a false one are equivalent </title>
(-> ph ps) , (-> ch ps)(-> (-. ps) (<-> ph ch))
pm5.21nii Eliminate an antecedent implied by each side of a biconditional. # <title> Eliminate an antecedent </title>
(-> ph ps) , (-> ch ps) , (-> ps (<-> ph ch))(<-> ph ch)
pm5.21nd Eliminate an antecedent implied by each side of a biconditional. # <title> Eliminate an antecedent </title>
(-> (/\ ph ps) th) , (-> (/\ ph ch) th) , (-> th (<-> ps ch))(-> ph (<-> ps ch))
bibif # <title> Transfer negation by equivalence </title>
(-> (-. ps) (<-> (<-> ph ps) (-. ph)))
pm5.35 Theorem *5.35 of [bib/WhiteheadRussell] p. 125.
(-> (/\ (-> ph ps) (-> ph ch)) (-> ph (<-> ps ch)))
pm5.54 Theorem *5.54 of [bib/WhiteheadRussell] p. 125.
(\/ (<-> (/\ ph ps) ph) (<-> (/\ ph ps) ps))
elimant Elimination of antecedents in an implication. (The proof was shortened by Juha Arpiainen, 19-Jan-2006.) # <title> Elimination antecedents in implication </title>
(-> (/\ (-> ph ps) (-> (-> ps ch) (-> ph th))) (-> ph (-> ch th)))
baib # <title> Move conjunction outside biconditional</title>
(<-> ph (/\ ps ch))(-> ps (<-> ph ch))
baibr # <title> Move conjunction outside biconditional</title>
(<-> ph (/\ ps ch))(-> ps (<-> ch ph))
pm5.44 Theorem *5.44 of [bib/WhiteheadRussell] p. 125.
(-> (-> ph ps) (<-> (-> ph ch) (-> ph (/\ ps ch))))
pm5.6 Conjunction in antecedent versus disjunction in consequent. Theorem *5.6 of [bib/WhiteheadRussell] p. 125. # <title> Conjunction in antecedent versus disjunction in consequent </title>
(<-> (-> (/\ ph (-. ps)) ch) (-> ph (\/ ps ch)))
nan # <title> Move a conjunct in and out of negation </title>
(<-> (-> ph (-. (/\ ps ch))) (-> (/\ ph ps) (-. ch)))
orcanai Change disjunction in consequent to conjunction in antecedent. # <title> Disjunction in consequent to conjunction in antecedent </title>
(-> ph (\/ ps ch))(-> (/\ ph (-. ps)) ch)
intnan Introduction of conjunct inside of a contradiction. # <title> Introduce conjunction inside contradiction </title>
(-. ph)(-. (/\ ps ph))
intnanr # <title> Introduce conjunction inside contradiction </title>
(-. ph)(-. (/\ ph ps))
intnand # <title> Introduce conjunction inside contradiction </title>
(-> ph (-. ps))(-> ph (-. (/\ ch ps)))
intnanrd # <title> Introduce conjunction inside contradiction </title>
(-> ph (-. ps))(-> ph (-. (/\ ps ch)))
mpan # <title> Modus ponens </title>
ph , (-> (/\ ph ps) ch)(-> ps ch)
mpan2 # <title> Remove the true part of a conjunction </title> # <table> # [ <r> ps ] # (-> (/\ ph [ <r> ps ] ) ch) # (-> ph ] ] ch) # </table>
ps , (-> (/\ ph ps) ch)(-> ph ch)
mp2an # <title> Modus Ponens </title> # <table> # ph ] ] ] ] # [ [ ps ] ] # (-> (/\ ph ] [ ps ] ) [ ch) # [ [ [ [ ch # </table>
ph , ps , (-> (/\ ph ps) ch)ch
mpani An inference based on modus ponens. # <title> Modus Ponens </title>
ps , (-> ph (-> (/\ ps ch) th))(-> ph (-> ch th))
mpan2i An inference based on modus ponens. # <title> Modus Ponens </title>
ch , (-> ph (-> (/\ ps ch) th))(-> ph (-> ps th))
mp2ani An inference based on modus ponens. # <title> Modus Ponens </title>
ps , ch , (-> ph (-> (/\ ps ch) th))(-> ph th)
mpand A deduction based on modus ponens. # <title> Modus Ponens </title>
(-> ph ps) , (-> ph (-> (/\ ps ch) th))(-> ph (-> ch th))
mpan2d A deduction based on modus ponens. # <title> Modus Ponens </title>
(-> ph ch) , (-> ph (-> (/\ ps ch) th))(-> ph (-> ps th))
mp2and A deduction based on modus ponens. # <title> Modus Ponens </title>
(-> ph ps) , (-> ph ch) , (-> ph (-> (/\ ps ch) th))(-> ph th)
mpdan An inference based on modus ponens. # <title> Modus Ponens </title>
(-> ph ps) , (-> (/\ ph ps) ch)(-> ph ch)
mpancom An inference based on modus ponens with commutation of antecedents. # <title> Modus Ponens & Commute </title>
(-> ps ph) , (-> (/\ ph ps) ch)(-> ps ch)
mpanl1 An inference based on modus ponens. # <title> Modus Ponens </title>
ph , (-> (/\ (/\ ph ps) ch) th)(-> (/\ ps ch) th)
mpanl2 An inference based on modus ponens. # <title> Modus Ponens </title>
ps , (-> (/\ (/\ ph ps) ch) th)(-> (/\ ph ch) th)
mpanl12 An inference based on modus ponens. # <title> Modus Ponens </title>
ph , ps , (-> (/\ (/\ ph ps) ch) th)(-> ch th)
mpanr1 An inference based on modus ponens. # <title> Modus Ponens </title>
ps , (-> (/\ ph (/\ ps ch)) th)(-> (/\ ph ch) th)
mpanr2 An inference based on modus ponens. # <title> Modus Ponens </title>
ch , (-> (/\ ph (/\ ps ch)) th)(-> (/\ ph ps) th)
mpanr12 An inference based on modus ponens. # <title> Modus Ponens </title>
ps , ch , (-> (/\ ph (/\ ps ch)) th)(-> ph th)
mpanlr1 An inference based on modus ponens. # <title> Modus Ponens </title>
ps , (-> (/\ (/\ ph (/\ ps ch)) th) ta)(-> (/\ (/\ ph ch) th) ta)
mtt Modus-tollens-like theorem. # <title> Modus Tollens </title>
(-> (-. ph) (<-> (-. ps) (-> ps ph)))
mt2bi A false consequent falsifies an antecedent. # <title> Modus Tollens </title>
ph(<-> (-. ps) (-> ps (-. ph)))
mtbid A deduction from a biconditional, similar to modus tollens. # <title> Modus Tollens </title>
(-> ph (-. ps)) , (-> ph (<-> ps ch))(-> ph (-. ch))
mtbird A deduction from a biconditional, similar to modus tollens. # <title> Modus Tollens </title>
(-> ph (-. ch)) , (-> ph (<-> ps ch))(-> ph (-. ps))
mtbii An inference from a biconditional, similar to modus tollens. # <title> Modus Tollens </title>
(-. ps) , (-> ph (<-> ps ch))(-> ph (-. ch))
mtbiri An inference from a biconditional, similar to modus tollens. # <title> Modus Tollens </title> # <table> # [ [ (-. [ ch) # (-> ph (<-> ps ] [ [ ch)) # (-> ph (-. ps ] ] ] )) # </table>
(-. ch) , (-> ph (<-> ps ch))(-> ph (-. ps))
2th # <title> Two truths are equivalent </title>
ph , ps(<-> ph ps)
2false # <title> Two falsehoods are equivalent </title>
(-. ph) , (-. ps)(<-> ph ps)
tbt A wff is equivalent to its equivalence with truth. (The proof was shortened by Juha Arpiainen, 19-Jan-2006.) # <title> Proposition is equivalent to its equivalence with truth </title>
ph(<-> ps (<-> ps ph))
nbn2 The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by Juha Arpiainen, 19-Jan-2006.) # <title> Negated Proposition is equivalent to falsehood </title>
(-> (-. ph) (<-> (-. ps) (<-> ph ps)))
nbn The negation of a wff is equivalent to the wff's equivalence to falsehood. # <title> Negated Proposition is equivalent to falsehood </title>
(-. ph)(<-> (-. ps) (<-> ps ph))
nbn3 # <title> Transfer falsehood via equivalence </title>
ph(<-> (-. ps) (<-> ps (-. ph)))
biantru A wff is equivalent to its conjunction with truth.
ph(<-> ps (/\ ps ph))
biantrur A wff is equivalent to its conjunction with truth.
ph(<-> ps (/\ ph ps))
biantrud A wff is equivalent to its conjunction with truth.
(-> ph ps)(-> ph (<-> ch (/\ ch ps)))
biantrurd A wff is equivalent to its conjunction with truth.
(-> ph ps)(-> ph (<-> ch (/\ ps ch)))
mpbiran Detach truth from conjunction in biconditional.
(<-> ph (/\ ps ch)) , ps(<-> ph ch)
mpbiran2 Detach truth from conjunction in biconditional.
(<-> ph (/\ ps ch)) , ch(<-> ph ps)
mpbir2an Detach a conjunction of truths in a biconditional.
(<-> ph (/\ ps ch)) , ps , chph
biimt A wff is equivalent to itself with true antecedent.
(-> ph (<-> ps (-> ph ps)))
pm5.5 Theorem *5.5 of [bib/WhiteheadRussell] p. 125.
(-> ph (<-> (-> ph ps) ps))
pm5.62 Theorem *5.62 of [bib/WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 21-Jun-2005.)
(<-> (\/ (/\ ph ps) (-. ps)) (\/ ph (-. ps)))
biort A wff is disjoined with truth is true.
(-> ph (<-> ph (\/ ph ps)))
biorf A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [bib/WhiteheadRussell] p. 121.
(-> (-. ph) (<-> ps (\/ ph ps)))
biorfi A wff is equivalent to its disjunction with falsehood.
(-. ph)(<-> ps (\/ ps ph))
bianfi A wff conjoined with falsehood is false.
(-. ph)(<-> ph (/\ ps ph))
bianfd A wff conjoined with falsehood is false.
(-> ph (-. ps))(-> ph (<-> ps (/\ ps ch)))
pm4.82 Theorem *4.82 of [bib/WhiteheadRussell] p. 122.
(<-> (/\ (-> ph ps) (-> ph (-. ps))) (-. ph))
pm4.83 Theorem *4.83 of [bib/WhiteheadRussell] p. 122.
(<-> (/\ (-> ph ps) (-> (-. ph) ps)) ps)
pclem6 Negation inferred from embedded conjunct.
(-> (<-> ph (/\ ps (-. ph))) (-. ps))
biantr A transitive law of equivalence. Compare Theorem *4.22 of [bib/WhiteheadRussell] p. 117.
(-> (/\ (<-> ph ps) (<-> ch ps)) (<-> ph ch))
orbidi Disjunction distributes over the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), [[http://citeseer.ist.psu.edu/lifschitz98calculational.html]].
(<-> (\/ ph (<-> ps ch)) (<-> (\/ ph ps) (\/ ph ch)))
biass Associative law for the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), [[http://citeseer.ist.psu.edu/lifschitz98calculational.html]]. Interestingly, this law was not included in //Principia Mathematica// but was apparently first noted by Jan Lukasiewicz circa 1923. (The proof was shortened by Juha Arpiainen, 19-Jan-2006.) # <title> Associative Property </title>
(<-> (<-> (<-> ph ps) ch) (<-> ph (<-> ps ch)))
biluk Lukasiewicz's shortest axiom for equivalential calculus. Storrs McCall, ed., //Polish Logic 1920-1939// (Oxford, 1967), p. 96.
(<-> (<-> ph ps) (<-> (<-> ch ps) (<-> ph ch)))
pm5.7 Disjunction distributes over the biconditional. Theorem *5.7 of [bib/WhiteheadRussell] p. 125. This theorem is similar to [[orbidi]]. (Contributed by Roy F. Longton, 21-Jun-2005.)
(<-> (<-> (\/ ph ch) (\/ ps ch)) (\/ ch (<-> ph ps)))
bigolden # <title> Dijkstra-Scholten's Golden Rule </title>
(<-> (<-> (/\ ph ps) ph) (<-> ps (\/ ph ps)))
pm5.71 Theorem *5.71 of [bib/WhiteheadRussell] p. 125. (Contributed by Roy F. Longton, 23-Jun-2005.)
(-> (-> ps (-. ch)) (<-> (/\ (\/ ph ps) ch) (/\ ph ch)))
pm5.75 Theorem *5.75 of [bib/WhiteheadRussell] p. 126.
(-> (/\ (-> ch (-. ps)) (<-> ph (\/ ps ch))) (<-> (/\ ph (-. ps)) ch))
bimsc1 # <title> Removal of conjunct from one side of an equivalence </title>
(-> (/\ (-> ph ps) (<-> ch (/\ ps ph))) (<-> ch ph))
ecase2d # <title> Elimination by cases </title>
(-> ph ps) , (-> ph (-. (/\ ps ch))) , (-> ph (-. (/\ ps th))) , (-> ph (\/ ta (\/ ch th)))(-> ph ta)
ecase3 # <title> Elimination by cases </title>
(-> ph ch) , (-> ps ch) , (-> (-. (\/ ph ps)) ch)ch
ecase # <title> Elimination by cases </title>
(-> (-. ph) ch) , (-> (-. ps) ch) , (-> (/\ ph ps) ch)ch
ecase3d # <title> Elimination by cases </title>
(-> ph (-> ps th)) , (-> ph (-> ch th)) , (-> ph (-> (-. (\/ ps ch)) th))(-> ph th)
ccase # <title> Elimination by cases </title>
(-> (/\ ph ps) ta) , (-> (/\ ch ps) ta) , (-> (/\ ph th) ta) , (-> (/\ ch th) ta)(-> (/\ (\/ ph ch) (\/ ps th)) ta)
ccased # <title> Elimination by cases </title>
(-> ph (-> (/\ ps ch) et)) , (-> ph (-> (/\ th ch) et)) , (-> ph (-> (/\ ps ta) et)) , (-> ph (-> (/\ th ta) et))(-> ph (-> (/\ (\/ ps th) (\/ ch ta)) et))
ccase2 # <title> Elimination by cases </title>
(-> (/\ ph ps) ta) , (-> ch ta) , (-> th ta)(-> (/\ (\/ ph ch) (\/ ps th)) ta)
4cases Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. # <title> Elimination by cases </title>
(-> (/\ ph ps) ch) , (-> (/\ ph (-. ps)) ch) , (-> (/\ (-. ph) ps) ch) , (-> (/\ (-. ph) (-. ps)) ch)ch
niabn Miscellaneous inference relating falsehoods.
ph(-> (-. ps) (<-> (/\ ch ps) (-. ph)))
dedlem0a Lemma for an alternate version of weak deduction theorem. # <title> Weak Deduction Theorem Lemma </title>
(-> ph (<-> ps (-> (-> ch ph) (/\ ps ph))))
dedlem0b Lemma for an alternate version of weak deduction theorem. # <title> Weak Deduction Theorem Lemma </title>
(-> (-. ph) (<-> ps (-> (-> ps ph) (/\ ch ph))))
dedlema # <title> Weak Deduction Theorem Lemma </title>
(-> ph (<-> ps (\/ (/\ ps ph) (/\ ch (-. ph)))))
dedlemb # <title> Weak Deduction Theorem Lemma </title>
(-> (-. ph) (<-> ch (\/ (/\ ps ph) (/\ ch (-. ph)))))
elimh Hypothesis builder for weak deduction theorem. For more information, see the Deduction Theorem link on the Metamath Proof Explorer home page. # <title> Hypothesis builder for weak deduction theorem </title>
(-> (<-> ph (\/ (/\ ph ch) (/\ ps (-. ch)))) (<-> ch ta)) , (-> (<-> ps (\/ (/\ ph ch) (/\ ps (-. ch)))) (<-> th ta)) , thta
dedt The weak deduction theorem. For more information, see the Deduction Theorem link on the Metamath Proof Explorer home page. # <title> Weak Deduction theorem </title>
(-> (<-> ph (\/ (/\ ph ch) (/\ ps (-. ch)))) (<-> th ta)) , ta(-> ch th)
con3th Contraposition. Theorem *2.16 of [bib/WhiteheadRussell] p. 103. This version of [[con3]] demonstrates the use of the weak deduction theorem to derive it from [[con3i]]. # <title> Contraposition </title>
(-> (-> ph ps) (-> (-. ps) (-. ph)))
consensus # <title> Consensus Theorem </title> # <summary> This theorem and its dual (with {{{\/}}} and {{{/\}}} interchanged) are commonly used in computer logic design to eliminate redundant terms from Boolean expressions. Specifically, we prove that the term #(/\ ps ch)# on the left-hand side is redundant. # </summary>
(<-> (\/ (\/ (/\ ph ps) (/\ (-. ph) ch)) (/\ ps ch)) (\/ (/\ ph ps) (/\ (-. ph) ch)))
pm4.42 Theorem *4.42 of [bib/WhiteheadRussell] p. 119. (Contributed by Roy F. Longton, 21-Jun-2005.)
(<-> ph (\/ (/\ ph ps) (/\ ph (-. ps))))
ninba Miscellaneous inference relating falsehoods.
ph(-> (-. ps) (<-> (-. ph) (/\ ch ps)))
prlem1 A specialized lemma for set theory (to derive the Axiom of Pairing).
(-> ph (<-> et ch)) , (-> ps (-. th))(-> ph (-> ps (-> (\/ (/\ ps ch) (/\ th ta)) et)))
prlem2 A specialized lemma for set theory (to derive the Axiom of Pairing).
(<-> (\/ (/\ ph ps) (/\ ch th)) (/\ (\/ ph ch) (\/ (/\ ph ps) (/\ ch th))))
oplem1 A specialized lemma for set theory (ordered pair theorem).
(-> ph (\/ ps ch)) , (-> ph (\/ th ta)) , (<-> ps th) , (-> ch (<-> th ta))(-> ph ps)
rnlem Lemma used in construction of real numbers.
(<-> (/\ (/\ ph ps) (/\ ch th)) (/\ (/\ (/\ ph ch) (/\ ps th)) (/\ (/\ ph th) (/\ ps ch))))
dn1 A single axiom for Boolean algebra known as DN_1. See [[http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf]]. (Contributed by Jeffrey Hankins, 3-Jul-2009.)
(<-> (-. (\/ (-. (\/ (-. (\/ ph ps)) ch)) (-. (\/ ph (-. (\/ (-. ch) (-. (\/ ch th)))))))) ch)
(<-> (\/\/ ph ps ch) (\/ (\/ ph ps) ch))
(<-> (/\/\ ph ps ch) (/\ (/\ ph ps) ch))
3orass Associative law for triple disjunction.
(<-> (\/\/ ph ps ch) (\/ ph (\/ ps ch)))
3anass Associative law for triple conjunction.
(<-> (/\/\ ph ps ch) (/\ ph (/\ ps ch)))
3anrot Rotation law for triple conjunction.
(<-> (/\/\ ph ps ch) (/\/\ ps ch ph))
3orrot Rotation law for triple disjunction.
(<-> (\/\/ ph ps ch) (\/\/ ps ch ph))
3ancoma Commutation law for triple conjunction.
(<-> (/\/\ ph ps ch) (/\/\ ps ph ch))
3ancomb Commutation law for triple conjunction.
(<-> (/\/\ ph ps ch) (/\/\ ph ch ps))
3anrev Reversal law for triple conjunction.
(<-> (/\/\ ph ps ch) (/\/\ ch ps ph))
3simpa Simplification of triple conjunction.
(-> (/\/\ ph ps ch) (/\ ph ps))
3simpb Simplification of triple conjunction.
(-> (/\/\ ph ps ch) (/\ ph ch))
3simpc Simplification of triple conjunction.
(-> (/\/\ ph ps ch) (/\ ps ch))
3simp1 Simplification of triple conjunction.
(-> (/\/\ ph ps ch) ph)
3simp2 Simplification of triple conjunction.
(-> (/\/\ ph ps ch) ps)
3simp3 Simplification of triple conjunction.
(-> (/\/\ ph ps ch) ch)
3simpl1 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
(-> (/\ (/\/\ ph ps ch) th) ph)
3simpl2 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
(-> (/\ (/\/\ ph ps ch) th) ps)
3simpl3 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
(-> (/\ (/\/\ ph ps ch) th) ch)
3simpr1 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
(-> (/\ ph (/\/\ ps ch th)) ps)
3simpr2 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
(-> (/\ ph (/\/\ ps ch th)) ch)
3simpr3 Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
(-> (/\ ph (/\/\ ps ch th)) th)
3simp1i Infer a conjunct from a triple conjunction.
(/\/\ ph ps ch)ph
3simp2i Infer a conjunct from a triple conjunction.
(/\/\ ph ps ch)ps
3simp3i Infer a conjunct from a triple conjunction.
(/\/\ ph ps ch)ch
3simp1d Deduce a conjunct from a triple conjunction.
(-> ph (/\/\ ps ch th))(-> ph ps)
3simp2d Deduce a conjunct from a triple conjunction.
(-> ph (/\/\ ps ch th))(-> ph ch)
3simp3d Deduce a conjunct from a triple conjunction.
(-> ph (/\/\ ps ch th))(-> ph th)
3adant1 Deduction adding a conjunct to antecedent.
(-> (/\ ph ps) ch)(-> (/\/\ th ph ps) ch)
3adant2 Deduction adding a conjunct to antecedent.
(-> (/\ ph ps) ch)(-> (/\/\ ph th ps) ch)
3adant3 Deduction adding a conjunct to antecedent.
(-> (/\ ph ps) ch)(-> (/\/\ ph ps th) ch)
3ad2ant1 Deduction adding conjuncts to an antecedent.
(-> ph ch)(-> (/\/\ ph ps th) ch)
3ad2ant2 Deduction adding conjuncts to an antecedent.
(-> ph ch)(-> (/\/\ ps ph th) ch)
3ad2ant3 Deduction adding conjuncts to an antecedent.
(-> ph ch)(-> (/\/\ ps th ph) ch)
3adantl1 Deduction adding a conjunct to antecedent.
(-> (/\ (/\ ph ps) ch) th)(-> (/\ (/\/\ ta ph ps) ch) th)
3adantl2 Deduction adding a conjunct to antecedent.
(-> (/\ (/\ ph ps) ch) th)(-> (/\ (/\/\ ph ta ps) ch) th)
3adantl3 Deduction adding a conjunct to antecedent.
(-> (/\ (/\ ph ps) ch) th)(-> (/\ (/\/\ ph ps ta) ch) th)
3adantr1 Deduction adding a conjunct to antecedent.
(-> (/\ ph (/\ ps ch)) th)(-> (/\ ph (/\/\ ta ps ch)) th)
3adantr2 Deduction adding a conjunct to antecedent.
(-> (/\ ph (/\ ps ch)) th)(-> (/\ ph (/\/\ ps ta ch)) th)
3adantr3 Deduction adding a conjunct to antecedent.
(-> (/\ ph (/\ ps ch)) th)(-> (/\ ph (/\/\ ps ch ta)) th)
(-> (/\ ph ch) th)(-> (/\ (/\/\ ph ps ta) ch) th)
(-> (/\ ph ch) th)(-> (/\ (/\/\ ps ph ta) ch) th)
(-> (/\ ph ch) th)(-> (/\ (/\/\ ps ta ph) ch) th)
3ad2antr1 Deduction adding a conjuncts to antecedent.
(-> (/\ ph ch) th)(-> (/\ ph (/\/\ ch ps ta)) th)
3ad2antr2 Deduction adding a conjuncts to antecedent.
(-> (/\ ph ch) th)(-> (/\ ph (/\/\ ps ch ta)) th)
3ad2antr3 Deduction adding a conjuncts to antecedent.
(-> (/\ ph ch) th)(-> (/\ ph (/\/\ ps ta ch)) th)
3mix1 Introduction in triple disjunction.
(-> ph (\/\/ ph ps ch))
3mix2 Introduction in triple disjunction.
(-> ph (\/\/ ps ph ch))
3mix3 Introduction in triple disjunction.
(-> ph (\/\/ ps ch ph))
3pm3.2i Infer conjunction of premises.
ph , ps , ch(/\/\ ph ps ch)
3jca Join consequents with conjunction.
(-> ph ps) , (-> ph ch) , (-> ph th)(-> ph (/\/\ ps ch th))
3jcad Deduction conjoining the consequents of three implications.
(-> ph (-> ps ch)) , (-> ph (-> ps th)) , (-> ph (-> ps ta))(-> ph (-> ps (/\/\ ch th ta)))
3anim123i Join antecedents and consequents with conjunction.
(-> ph ps) , (-> ch th) , (-> ta et)(-> (/\/\ ph ch ta) (/\/\ ps th et))
3anbi123i Join 3 biconditionals with conjunction.
(<-> ph ps) , (<-> ch th) , (<-> ta et)(<-> (/\/\ ph ch ta) (/\/\ ps th et))
3orbi123i Join 3 biconditionals with disjunction.
(<-> ph ps) , (<-> ch th) , (<-> ta et)(<-> (\/\/ ph ch ta) (\/\/ ps th et))
3anbi1i Inference adding two conjuncts to each side of a biconditional.
(<-> ph ps)(<-> (/\/\ ph ch th) (/\/\ ps ch th))
3anbi2i Inference adding two conjuncts to each side of a biconditional.
(<-> ph ps)(<-> (/\/\ ch ph th) (/\/\ ch ps th))
3anbi3i Inference adding two conjuncts to each side of a biconditional.
(<-> ph ps)(<-> (/\/\ ch th ph) (/\/\ ch th ps))
3imp Importation inference.
(-> ph (-> ps (-> ch th)))(-> (/\/\ ph ps ch) th)
3impa Importation from double to triple conjunction.
(-> (/\ (/\ ph ps) ch) th)(-> (/\/\ ph ps ch) th)
3impb Importation from double to triple conjunction.
(-> (/\ ph (/\ ps ch)) th)(-> (/\/\ ph ps ch) th)
3impia Importation to triple conjunction.
(-> (/\ ph ps) (-> ch th))(-> (/\/\ ph ps ch) th)
3impib Importation to triple conjunction.
(-> ph (-> (/\ ps ch) th))(-> (/\/\ ph ps ch) th)
3exp Exportation inference.
(-> (/\/\ ph ps ch) th)(-> ph (-> ps (-> ch th)))
3expa Exportation from triple to double conjunction.
(-> (/\/\ ph ps ch) th)(-> (/\ (/\ ph ps) ch) th)
3expb Exportation from triple to double conjunction.
(-> (/\/\ ph ps ch) th)(-> (/\ ph (/\ ps ch)) th)
3expia Exportation from triple conjunction.
(-> (/\/\ ph ps ch) th)(-> (/\ ph ps) (-> ch th))
3expib Exportation from triple conjunction.
(-> (/\/\ ph ps ch) th)(-> ph (-> (/\ ps ch) th))
3com12 Commutation in antecedent. Swap 1st and 3rd.
(-> (/\/\ ph ps ch) th)(-> (/\/\ ps ph ch) th)
3com13 Commutation in antecedent. Swap 1st and 3rd.
(-> (/\/\ ph ps ch) th)(-> (/\/\ ch ps ph) th)
3com23 Commutation in antecedent. Swap 2nd and 3rd.
(-> (/\/\ ph ps ch) th)(-> (/\/\ ph ch ps) th)
3coml Commutation in antecedent. Rotate left.
(-> (/\/\ ph ps ch) th)(-> (/\/\ ps ch ph) th)
3comr Commutation in antecedent. Rotate right.
(-> (/\/\ ph ps ch) th)(-> (/\/\ ch ph ps) th)
3adant3r1 Deduction adding a conjunct to antecedent.
(-> (/\/\ ph ps ch) th)(-> (/\ ph (/\/\ ta ps ch)) th)
3adant3r2 Deduction adding a conjunct to antecedent.
(-> (/\/\ ph ps ch) th)(-> (/\ ph (/\/\ ps ta ch)) th)
3adant3r3 Deduction adding a conjunct to antecedent.
(-> (/\/\ ph ps ch) th)(-> (/\ ph (/\/\ ps ch ta)) th)
3an1rs Swap conjuncts.
(-> (/\ (/\/\ ph ps ch) th) ta)(-> (/\ (/\/\ ph ps th) ch) ta)
3imp1 Importation to left triple conjunction.
(-> ph (-> ps (-> ch (-> th ta))))(-> (/\ (/\/\ ph ps ch) th) ta)
3impd Importation deduction for triple conjunction.
(-> ph (-> ps (-> ch (-> th ta))))(-> ph (-> (/\/\ ps ch th) ta))
3imp2 Importation to right triple conjunction.
(-> ph (-> ps (-> ch (-> th ta))))(-> (/\ ph (/\/\ ps ch th)) ta)
3exp1 Exportation from left triple conjunction.
(-> (/\ (/\/\ ph ps ch) th) ta)(-> ph (-> ps (-> ch (-> th ta))))
3expd Exportation deduction for triple conjunction.
(-> ph (-> (/\/\ ps ch th) ta))(-> ph (-> ps (-> ch (-> th ta))))
3exp2 Exportation from right triple conjunction.
(-> (/\ ph (/\/\ ps ch th)) ta)(-> ph (-> ps (-> ch (-> th ta))))
3adant1l Deduction adding a conjunct to antecedent.
(-> (/\/\ ph ps ch) th)(-> (/\/\ (/\ ta ph) ps ch) th)
3adant1r Deduction adding a conjunct to antecedent.
(-> (/\/\ ph ps ch) th)(-> (/\/\ (/\ ph ta) ps ch) th)
3adant2l Deduction adding a conjunct to antecedent.
(-> (/\/\ ph ps ch) th)(-> (/\/\ ph (/\ ta ps) ch) th)
3adant2r Deduction adding a conjunct to antecedent.
(-> (/\/\ ph ps ch) th)(-> (/\/\ ph (/\ ps ta) ch) th)
3adant3l Deduction adding a conjunct to antecedent.
(-> (/\/\ ph ps ch) th)(-> (/\/\ ph ps (/\ ta ch)) th)
3adant3r Deduction adding a conjunct to antecedent.
(-> (/\/\ ph ps ch) th)(-> (/\/\ ph ps (/\ ch ta)) th)
syl3anc A syllogism inference combined with contraction.
(-> (/\/\ ph ps ch) th) , (-> ta ph) , (-> ta ps) , (-> ta ch)(-> ta th)
syl3an1 A syllogism inference.
(-> (/\/\ ph ps ch) th) , (-> ta ph)(-> (/\/\ ta ps ch) th)
syl3an2 A syllogism inference.
(-> (/\/\ ph ps ch) th) , (-> ta ps)(-> (/\/\ ph ta ch) th)
syl3an3 A syllogism inference.
(-> (/\/\ ph ps ch) th) , (-> ta ch)(-> (/\/\ ph ps ta) th)
syl3an1b A syllogism inference.
(-> (/\/\ ph ps ch) th) , (<-> ta ph)(-> (/\/\ ta ps ch) th)
syl3an2b A syllogism inference.
(-> (/\/\ ph ps ch) th) , (<-> ta ps)(-> (/\/\ ph ta ch) th)
syl3an3b A syllogism inference.
(-> (/\/\ ph ps ch) th) , (<-> ta ch)(-> (/\/\ ph ps ta) th)
syl3an1br A syllogism inference.
(-> (/\/\ ph ps ch) th) , (<-> ph ta)(-> (/\/\ ta ps ch) th)
syl3an2br A syllogism inference.
(-> (/\/\ ph ps ch) th) , (<-> ps ta)(-> (/\/\ ph ta ch) th)
syl3an3br A syllogism inference.
(-> (/\/\ ph ps ch) th) , (<-> ch ta)(-> (/\/\ ph ps ta) th)
syl3an A triple syllogism inference.
(-> (/\/\ ph ps ch) th) , (-> ta ph) , (-> et ps) , (-> ze ch)(-> (/\/\ ta et ze) th)
syl3anb A triple syllogism inference.
(-> (/\/\ ph ps ch) th) , (<-> ta ph) , (<-> et ps) , (<-> ze ch)(-> (/\/\ ta et ze) th)
syld3an3 A syllogism inference.
(-> (/\/\ ph ps ch) th) , (-> (/\/\ ph ps ta) ch)(-> (/\/\ ph ps ta) th)
syld3an1 A syllogism inference.
(-> (/\/\ ph ps ch) th) , (-> (/\/\ ta ps ch) ph)(-> (/\/\ ta ps ch) th)
syld3an2 A syllogism inference.
(-> (/\/\ ph ps ch) th) , (-> (/\/\ ph ta ch) ps)(-> (/\/\ ph ta ch) th)
syl3anl1 A syllogism inference.
(-> (/\ (/\/\ ph ps ch) th) ta) , (-> et ph)(-> (/\ (/\/\ et ps ch) th) ta)
syl3anl2 A syllogism inference.
(-> (/\ (/\/\ ph ps ch) th) ta) , (-> et ps)(-> (/\ (/\/\ ph et ch) th) ta)
syl3anl3 A syllogism inference.
(-> (/\ (/\/\ ph ps ch) th) ta) , (-> et ch)(-> (/\ (/\/\ ph ps et) th) ta)
syl3anl A triple syllogism inference.
(-> (/\ (/\/\ ph ps ch) th) ta) , (-> et ph) , (-> ze ps) , (-> si ch)(-> (/\ (/\/\ et ze si) th) ta)
syl3anr1 A syllogism inference.
(-> (/\ ph (/\/\ ps ch th)) ta) , (-> et ps)(-> (/\ ph (/\/\ et ch th)) ta)
syl3anr2 A syllogism inference.
(-> (/\ ph (/\/\ ps ch th)) ta) , (-> et ch)(-> (/\ ph (/\/\ ps et th)) ta)
syl3anr3 A syllogism inference.
(-> (/\ ph (/\/\ ps ch th)) ta) , (-> et th)(-> (/\ ph (/\/\ ps ch et)) ta)
3impdi Importation inference (undistribute conjunction).
(-> (/\ (/\ ph ps) (/\ ph ch)) th)(-> (/\/\ ph ps ch) th)
3impdir Importation inference (undistribute conjunction).
(-> (/\ (/\ ph ps) (/\ ch ps)) th)(-> (/\/\ ph ch ps) th)
3anidm12 Inference from idempotent law for conjunction.
(-> (/\/\ ph ph ps) ch)(-> (/\ ph ps) ch)
3anidm13 Inference from idempotent law for conjunction.
(-> (/\/\ ph ps ph) ch)(-> (/\ ph ps) ch)
3anidm23 Inference from idempotent law for conjunction.
(-> (/\/\ ph ps ps) ch)(-> (/\ ph ps) ch)
3ori Infer implication from triple disjunction.
(\/\/ ph ps ch)(-> (/\ (-. ph) (-. ps)) ch)
3jao Disjunction of 3 antecedents.
(-> (/\/\ (-> ph ps) (-> ch ps) (-> th ps)) (-> (\/\/ ph ch th) ps))
3jaoi Disjunction of 3 antecedents (inference).
(-> ph ps) , (-> ch ps) , (-> th ps)(-> (\/\/ ph ch th) ps)
3jaod Disjunction of 3 antecedents (deduction).
(-> ph (-> ps ch)) , (-> ph (-> th ch)) , (-> ph (-> ta ch))(-> ph (-> (\/\/ ps th ta) ch))
3jaoian Disjunction of 3 antecedents (inference).
(-> (/\ ph ps) ch) , (-> (/\ th ps) ch) , (-> (/\ ta ps) ch)(-> (/\ (\/\/ ph th ta) ps) ch)
3jaodan Disjunction of 3 antecedents (deduction).
(-> (/\ ph ps) ch) , (-> (/\ ph th) ch) , (-> (/\ ph ta) ch)(-> (/\ ph (\/\/ ps th ta)) ch)
syl3an9b Nested syllogism inference conjoining 3 dissimilar antecedents.
(-> ph (<-> ps ch)) , (-> th (<-> ch ta)) , (-> et (<-> ta ze))(-> (/\/\ ph th et) (<-> ps ze))
3orbi123d Deduction joining 3 equivalences to form equivalence of disjunctions.
(-> ph (<-> ps ch)) , (-> ph (<-> th ta)) , (-> ph (<-> et ze))(-> ph (<-> (\/\/ ps th et) (\/\/ ch ta ze)))
3anbi123d Deduction joining 3 equivalences to form equivalence of conjunctions.
(-> ph (<-> ps ch)) , (-> ph (<-> th ta)) , (-> ph (<-> et ze))(-> ph (<-> (/\/\ ps th et) (/\/\ ch ta ze)))
3anbi12d Deduction conjoining and adding a conjunct to equivalences.
(-> ph (<-> ps ch)) , (-> ph (<-> th ta))(-> ph (<-> (/\/\ ps th et) (/\/\ ch ta et)))
3anbi13d Deduction conjoining and adding a conjunct to equivalences.
(-> ph (<-> ps ch)) , (-> ph (<-> th ta))(-> ph (<-> (/\/\ ps et th) (/\/\ ch et ta)))
3anbi23d Deduction conjoining and adding a conjunct to equivalences.
(-> ph (<-> ps ch)) , (-> ph (<-> th ta))(-> ph (<-> (/\/\ et ps th) (/\/\ et ch ta)))
3anbi1d Deduction adding conjuncts to an equivalence.
(-> ph (<-> ps ch))(-> ph (<-> (/\/\ ps th ta) (/\/\ ch th ta)))
3anbi2d Deduction adding conjuncts to an equivalence.
(-> ph (<-> ps ch))(-> ph (<-> (/\/\ th ps ta) (/\/\ th ch ta)))
3anbi3d Deduction adding conjuncts to an equivalence.
(-> ph (<-> ps ch))(-> ph (<-> (/\/\ th ta ps) (/\/\ th ta ch)))
3anim123d Deduction joining 3 implications to form implication of conjunctions.
(-> ph (-> ps ch)) , (-> ph (-> th ta)) , (-> ph (-> et ze))(-> ph (-> (/\/\ ps th et) (/\/\ ch ta ze)))
3orim123d Deduction joining 3 implications to form implication of disjunctions.
(-> ph (-> ps ch)) , (-> ph (-> th ta)) , (-> ph (-> et ze))(-> ph (-> (\/\/ ps th et) (\/\/ ch ta ze)))
an6 Rearrangement of 6 conjuncts.
(<-> (/\ (/\/\ ph ps ch) (/\/\ th ta et)) (/\/\ (/\ ph th) (/\ ps ta) (/\ ch et)))
mp3an1 An inference based on modus ponens.
ph , (-> (/\/\ ph ps ch) th)(-> (/\ ps ch) th)
mp3an2 An inference based on modus ponens.
ps , (-> (/\/\ ph ps ch) th)(-> (/\ ph ch) th)
mp3an3 An inference based on modus ponens.
ch , (-> (/\/\ ph ps ch) th)(-> (/\ ph ps) th)
mp3an12 An inference based on modus ponens.
ph , ps , (-> (/\/\ ph ps ch) th)(-> ch th)
mp3an13 An inference based on modus ponens.
ph , ch , (-> (/\/\ ph ps ch) th)(-> ps th)
mp3an23 An inference based on modus ponens.
ps , ch , (-> (/\/\ ph ps ch) th)(-> ph th)
mp3an1i An inference based on modus ponens.
ps , (-> ph (-> (/\/\ ps ch th) ta))(-> ph (-> (/\ ch th) ta))
mp3anl1 An inference based on modus ponens.
ph , (-> (/\ (/\/\ ph ps ch) th) ta)(-> (/\ (/\ ps ch) th) ta)
mp3anl2 An inference based on modus ponens.
ps , (-> (/\ (/\/\ ph ps ch) th) ta)(-> (/\ (/\ ph ch) th) ta)
mp3anl3 An inference based on modus ponens.
ch , (-> (/\ (/\/\ ph ps ch) th) ta)(-> (/\ (/\ ph ps) th) ta)
mp3anr1 An inference based on modus ponens.
ps , (-> (/\ ph (/\/\ ps ch th)) ta)(-> (/\ ph (/\ ch th)) ta)
mp3anr2 An inference based on modus ponens.
ch , (-> (/\ ph (/\/\ ps ch th)) ta)(-> (/\ ph (/\ ps th)) ta)
mp3anr3 An inference based on modus ponens.
th , (-> (/\ ph (/\/\ ps ch th)) ta)(-> (/\ ph (/\ ps ch)) ta)
mp3an An inference based on modus ponens.
ph , ps , ch , (-> (/\/\ ph ps ch) th)th
mpd3an3 An inference based on modus ponens.
(-> (/\ ph ps) ch) , (-> (/\/\ ph ps ch) th)(-> (/\ ph ps) th)
mpd3an23 An inference based on modus ponens.
(-> ph ps) , (-> ph ch) , (-> (/\/\ ph ps ch) th)(-> ph th)
biimp3a Infer implication from a logical equivalence. Similar to [[biimpa]].
(-> (/\ ph ps) (<-> ch th))(-> (/\/\ ph ps ch) th)
biimp3ar Infer implication from a logical equivalence. Similar to [[biimpar]].
(-> (/\ ph ps) (<-> ch th))(-> (/\/\ ph ps th) ch)
3anandis Inference that undistributes a triple conjunction in the antecedent.
(-> (/\/\ (/\ ph ps) (/\ ph ch) (/\ ph th)) ta)(-> (/\ ph (/\/\ ps ch th)) ta)
3anandirs Inference that undistributes a triple conjunction in the antecedent.
(-> (/\/\ (/\ ph th) (/\ ps th) (/\ ch th)) ta)(-> (/\ (/\/\ ph ps ch) th) ta)
ecase23d Deduction for elimination by cases.
(-> ph (-. ch)) , (-> ph (-. th)) , (-> ph (\/\/ ps ch th))(-> ph ps)
3ecase Inference for elimination by cases.
(-> (-. ph) th) , (-> (-. ps) th) , (-> (-. ch) th) , (-> (/\/\ ph ps ch) th)th
meredith # <title> Meredith's sole axiom for propositional calculus </title> # <summary> # Carew Meredith's sole axiom for propositional calculus. This amazing # formula is thought to be the shortest possible single axiom for # propositional calculus with inference rule [[ax-mp]], where negation and # implication are primitive. Here we prove Meredith's axiom from [[ax-1]], # [[ax-2]], and [[ax-3]]. Then from it we derive the Lukasiewicz axioms # [[luk-1]], [[luk-2]], and [[luk-3]]. Using these we finally re-derive our # axioms as [[ax1]], [[ax2]], and [[ax3]], thus proving the equivalence of # all three systems. C. A. Meredith, "Single Axioms for the Systems # (C,N), (C,O) and (A,N) of the Two-Valued Propositional Calculus," //The # Journal of Computing Systems// vol. 1 (1953), pp. 155-164. Meredith # claimed to be close to a proof that this axiom is the shortest possible, # but the proof was apparently never completed. # # An obscure Irish lecturer, Meredith (1904-1976) became enamored with # logic somewhat late in life after attending talks by Lukasiewicz and # produced many remarkable results such as this axiom. From his obituary: # "He did logic whenever time and opportunity presented themselves, and he # did it on whatever materials came to hand: in a pub, his favored pint # of porter within reach, he would use the inside of cigarette packs to # write proofs for logical colleagues." # </summary>
(-> (-> (-> (-> (-> ph ps) (-> (-. ch) (-. th))) ch) ta) (-> (-> ta ph) (-> th ph)))
merlem1 Step 3 of Meredith's proof of Lukasiewicz axioms from his sole axiom. (The step numbers refer to Meredith's original paper.)
(-> (-> (-> ch (-> (-. ph) ps)) ta) (-> ph ta))
merlem2 Step 4 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
(-> (-> (-> ph ph) ch) (-> th ch))
merlem3 Step 7 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
(-> (-> (-> ps ch) ph) (-> ch ph))
merlem4 Step 8 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
(-> ta (-> (-> ta ph) (-> th ph)))
merlem5 Step 11 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
(-> (-> ph ps) (-> (-. (-. ph)) ps))
merlem6 Step 12 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
(-> ch (-> (-> (-> ps ch) ph) (-> th ph)))
merlem7 Between steps 14 and 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
(-> ph (-> (-> (-> ps ch) th) (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th)))
merlem8 Step 15 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
(-> (-> (-> ps ch) th) (-> (-> (-> ch ta) (-> (-. th) (-. ps))) th))
merlem9 Step 18 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
(-> (-> (-> ph ps) (-> ch (-> th (-> ps ta)))) (-> et (-> ch (-> th (-> ps ta)))))
merlem10 Step 19 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
(-> (-> ph (-> ph ps)) (-> th (-> ph ps)))
merlem11 Step 20 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
(-> (-> ph (-> ph ps)) (-> ph ps))
merlem12 Step 28 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
(-> (-> (-> th (-> (-. (-. ch)) ch)) ph) ph)
merlem13 Step 35 of Meredith's proof of Lukasiewicz axioms from his sole axiom.
(-> (-> ph ps) (-> (-> (-> th (-> (-. (-. ch)) ch)) (-. (-. ph))) ps))
luk-1 1 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
(-> (-> ph ps) (-> (-> ps ch) (-> ph ch)))
luk-2 2 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
(-> (-> (-. ph) ph) ph)
luk-3 3 of 3 axioms for propositional calculus due to Lukasiewicz, derived from Meredith's sole axiom.
(-> ph (-> (-. ph) ps))
luklem1 Used to rederive standard propositional axioms from Lukasiewicz'.
(-> ph ps) , (-> ps ch)(-> ph ch)
luklem2 Used to rederive standard propositional axioms from Lukasiewicz'.
(-> (-> ph (-. ps)) (-> (-> (-> ph ch) th) (-> ps th)))
luklem3 Used to rederive standard propositional axioms from Lukasiewicz'.
(-> ph (-> (-> (-> (-. ph) ps) ch) (-> th ch)))
luklem4 Used to rederive standard propositional axioms from Lukasiewicz'.
(-> (-> (-> (-> (-. ph) ph) ph) ps) ps)
luklem5 Used to rederive standard propositional axioms from Lukasiewicz'.
(-> ph (-> ps ph))
luklem6 Used to rederive standard propositional axioms from Lukasiewicz'.
(-> (-> ph (-> ph ps)) (-> ph ps))
luklem7 Used to rederive standard propositional axioms from Lukasiewicz'.
(-> (-> ph (-> ps ch)) (-> ps (-> ph ch)))
luklem8 Used to rederive standard propositional axioms from Lukasiewicz'.
(-> (-> ph ps) (-> (-> ch ph) (-> ch ps)))
ax1 Standard propositional axiom derived from Lukasiewicz axioms.
(-> ph (-> ps ph))
ax2 Standard propositional axiom derived from Lukasiewicz axioms.
(-> (-> ph (-> ps ch)) (-> (-> ph ps) (-> ph ch)))
ax3 Standard propositional axiom derived from Lukasiewicz axioms.
(-> (-> (-. ph) (-. ps)) (-> ps ph))
(<-> (-/\ ph ps) (-. (/\ ph ps)))
nic-justlem Lemma for handling nested 'nand's.
(<-> (-/\ ph (-/\ ch ps)) (-> ph (/\ ch ps)))
nic-justim Show equivalence between implication and the Nicod version. To derive [[nic-dfim]], apply [[nic-justbi]].
(<-> (-> ph ps) (-/\ ph (-/\ ps ps)))
nic-justneg Show equivalence between negation and the Nicod version. To derive [[nic-dfneg]], apply [[nic-justbi]].
(<-> (-. ps) (-/\ ps ps))
nic-justbi Show equivalence between the bidirectional and the Nicod version. (Contributed by Jeff Hoffman, 19-Nov-2007.)
(<-> (<-> ph ps) (-/\ (-/\ ph ps) (-/\ (-/\ ph ph) (-/\ ps ps))))
nic-dfim Define implication in terms of 'nand'. Analogous to #(<-> (-/\ ph (-/\ ps ps)) (-> ph ps))#. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition (\$a statement).
(-/\ (-/\ (-/\ ph (-/\ ps ps)) (-> ph ps)) (-/\ (-/\ (-/\ ph (-/\ ps ps)) (-/\ ph (-/\ ps ps))) (-/\ (-> ph ps) (-> ph ps))))
nic-dfneg Define negation in terms of 'nand'. Analogous to #(<-> (-/\ ph ph) (-. ph))#. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition (\$a statement).
(-/\ (-/\ (-/\ ph ph) (-. ph)) (-/\ (-/\ (-/\ ph ph) (-/\ ph ph)) (-/\ (-. ph) (-. ph))))
nic-mp Derive Nicod's rule of modus ponens using 'nand', from the standard one. Although the major and minor premise together also imply #ch#, this form is necessary for useful derivations from [[nic-ax]]. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom (\$a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.)
ph , (-/\ ph (-/\ ch ps))ps
nic-mpALT A direct proof of [[nic-mp]].
ph , (-/\ ph (-/\ ch ps))ps
nic-ax Nicod's axiom derived from the standard ones. See //Intro. to Math. Phil.// by B. Russell, p. 152. Like [[meredith]], the usual axioms can be derived from this and vice versa. Unlike [[meredith]], Nicod uses a different connective ('nand'), so another form of modus ponens must be used in proofs, e.g. {{{{}}} [[nic-ax]], [[nic-mp]] {{{}}}} is equivalent to {{{{}}} [[luk-1]], [[luk-2]], [[luk-3]], [[ax-mp]] {{{}}}}. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to an axiom (\$a statement). (Contributed by Jeff Hoffman, 19-Nov-2007.)
(-/\ (-/\ ph (-/\ ch ps)) (-/\ (-/\ ta (-/\ ta ta)) (-/\ (-/\ th ch) (-/\ (-/\ ph th) (-/\ ph th)))))
nic-axALT A direct proof of [[nic-ax]].
(-/\ (-/\ ph (-/\ ch ps)) (-/\ (-/\ ta (-/\ ta ta)) (-/\ (-/\ th ch) (-/\ (-/\ ph th) (-/\ ph th)))))
nic-imp Inference for [[nic-mp]] using [[nic-ax]] as major premise. (Contributed by Jeff Hoffman, 17-Nov-2007.)
(-/\ ph (-/\ ch ps))(-/\ (-/\ th ch) (-/\ (-/\ ph th) (-/\ ph th)))
nic-idlem1 Lemma for [[nic-id]].
(-/\ (-/\ th (-/\ ta (-/\ ta ta))) (-/\ (-/\ (-/\ ph (-/\ ch ps)) th) (-/\ (-/\ ph (-/\ ch ps)) th)))
nic-idlem2 Lemma for [[nic-id]]. Inference used by [[nic-id]].
(-/\ et (-/\ (-/\ ph (-/\ ch ps)) th))(-/\ (-/\ th (-/\ ta (-/\ ta ta))) et)
nic-id Theorem [[id]] expressed with {{{-/\}}}. (Contributed by Jeff Hoffman, 17-Nov-2007.)
(-/\ ta (-/\ ta ta))
nic-swap {{{-/\}}} is symmetric. (Contributed by Jeff Hoffman, 17-Nov-2007.)
(-/\ (-/\ th ph) (-/\ (-/\ ph th) (-/\ ph th)))
nic-isw1 Inference version of [[nic-swap]]. (Contributed by Jeff Hoffman, 17-Nov-2007.)
(-/\ th ph)(-/\ ph th)
nic-isw2 Inference for swapping nested terms. (Contributed by Jeff Hoffman, 17-Nov-2007.)
(-/\ ps (-/\ th ph))(-/\ ps (-/\ ph th))
nic-iimp1 Inference version of [[nic-imp]] using right-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.)
(-/\ ph (-/\ ch ps)) , (-/\ th ch)(-/\ th ph)
nic-iimp2 Inference version of [[nic-imp]] using left-handed term. (Contributed by Jeff Hoffman, 17-Nov-2007.)
(-/\ (-/\ ph ps) (-/\ ch ch)) , (-/\ th ph)(-/\ th (-/\ ch ch))
nic-idel Inference to remove the trailing term. (Contributed by Jeff Hoffman, 17-Nov-2007.)
(-/\ ph (-/\ ch ps))(-/\ ph (-/\ ch ch))
nic-ich Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.)
(-/\ ph (-/\ ps ps)) , (-/\ ps (-/\ ch ch))(-/\ ph (-/\ ch ch))
nic-idbl Double the terms. Since doubling is the same as negation, this can be viewed as a contraposition Inference. (Contributed by Jeff Hoffman, 17-Nov-2007.)
(-/\ ph (-/\ ps ps))(-/\ (-/\ ps ps) (-/\ (-/\ ph ph) (-/\ ph ph)))
nic-bijust For nic-* definitions, the biconditional connective is not used. Instead, definitions are made based on this form. [[nic-bi1]] and [[nic-bi2]] are used to convert the definitions into usable theorems about one side of the implication. (Contributed by Jeff Hoffman, 18-Nov-2007.)
(-/\ (-/\ ta ta) (-/\ (-/\ ta ta) (-/\ ta ta)))
nic-bi1 Inference to extract one side of an implication from a definition
(-/\ (-/\ ph ps) (-/\ (-/\ ph ph) (-/\ ps ps)))(-/\ ph (-/\ ps ps))
nic-bi2 Inference to extract the other side of an implication from a 'biconditional' definition.
(-/\ (-/\ ph ps) (-/\ (-/\ ph ph) (-/\ ps ps)))(-/\ ps (-/\ ph ph))
nic-stdmp Derive the standard modus ponens from [[nic-mp]]. (Contributed by Jeff Hoffman, 18-Nov-2007.)
ph , (-> ph ps)ps
nic-luk1 Proof of [[luk-1]] from [[nic-ax]] and [[nic-mp]] (and definitions [[nic-dfim]] and [[nic-dfneg]]). Note that the standard axioms [[ax-1]], [[ax-2]], and [[ax-3]] are proved from the Lukasiewicz axioms by theorems [[ax1]], [[ax2]], and [[ax3]]. (Contributed by Jeff Hoffman, 18-Nov-2007.)
(-> (-> ph ps) (-> (-> ps ch) (-> ph ch)))
nic-luk2 Proof of [[luk-2]] from [[nic-ax]] and [[nic-mp]]. (Contributed by Jeff Hoffman, 18-Nov-2007.)
(-> (-> (-. ph) ph) ph)
nic-luk3 Proof of [[luk-3]] from [[nic-ax]] and [[nic-mp]]. (Contributed by Jeff Hoffman, 18-Nov-2007.)
(-> ph (-> (-. ph) ps))
anbi2 ### END METAMATH DUMP ###
(-> (<-> ph ps) (<-> (/\ ch ph) (/\ ch ps)))
con4biir Reverse the hypothesis and conclusion of con4bii. # <title> Equivalence over Negation </title> # <table> # (<-> [ ph ] [ ps ] ) # (<-> (-. [ ph ] ) (-. [ ps ] )) # </table>
(<-> ph ps)(<-> (-. ph) (-. ps))
sylbi2 Reorder sylbi a bit. # <title> Syllogism </title> # <table> # (-> ps ] ] ] ch) # (<-> ps ] [ ph ] ) # (-> [ [ ph ] ch) # </table>
(-> ps ch) , (<-> ps ph)(-> ph ch)
(-> ph ps)(-> (<-> ch ph) (-> ch ps))
biim1i # <summary> The Order reverses which may be a little unexpected. </summary>
(-> ph ps)(-> (<-> ph ch) (-> ch ps))
bitr3icom Commute the conclusion of bitr3i. # <title> Transitive Property </title> # <table> # (<-> ps [ [ [ ph ] ) # (<-> ps [ ch ] ] ] ) # [ (<-> ch ] [ ph ] ) # </table>
(<-> ps ph) , (<-> ps ch)(<-> ch ph)
orbi1ii # <title> Equivalence over Disjunction </title> # <table> # (\/ ph ] ] ] ps) # (<-> ph ] [ ch ] ) # (\/ [ [ ch ] ps) # </table>
(\/ ph ps) , (<-> ph ch)(\/ ch ps)
orbi2ii # <title> Equivalence over Disjunction </title> # <table> # (\/ ph [ ps ] ] ] ) # (<-> [ ps ] [ ch ] ) # (\/ ph [ [ [ ch ] ) # </table>
(\/ ph ps) , (<-> ps ch)(\/ ph ch)
anbi1ii # <title> Equivalence over Conjunction </title> # <table> # (/\ ph ] ] ] ps) # (<-> ph ] [ ch ] ) # (\/ [ [ ch ] ps) # </table>
(/\ ph ps) , (<-> ph ch)(/\ ch ps)
anbi2ii # <title> Equivalence over Conjunction </title> # <table> # (/\ ph [ ps ] ] ] ) # (<-> [ ps ] [ ch ] ) # (/\ ph [ [ [ ch ] ) # </table>
(/\ ph ps) , (<-> ps ch)(/\ ph ch)
orassi # <title> Associative Property </title>
(\/ (\/ ph ps) ch)(\/ ph (\/ ps ch))
orassli # <title> Associative Property </title>
(\/ ph (\/ ps ch))(\/ (\/ ph ps) ch)
anassi # <title> Associative Property </title>
(/\ (/\ ph ps) ch)(/\ ph (/\ ps ch))
anassli # <title> Associative Property </title>
(/\ ph (/\ ps ch))(/\ (/\ ph ps) ch)
biassi # <title> Associative Property </title>
(<-> (<-> ph ps) ch)(<-> ph (<-> ps ch))
biassli # <title> Associative Property </title>
(<-> ph (<-> ps ch))(<-> (<-> ph ps) ch)
(-> (/\ ph (-. ps)) (-. (<-> ps ph)))
(-> (/\ ps (-. ph)) (-. (<-> ps ph)))
df-fal # <title> Definition of False </title> # <suggest> auto-left('Simplify', 'F') </suggest>
(<-> (F) (-. (T)))
notfal # <title> F is false </title>
(-. (F))
ax-mpRemove # <title> Modus Ponens </title> # <summary> ax-mp with the order of the first and second hypotheses reversed. </summary> # <table> # (-> ph ] [ ps) # ph ] ] # [ [ ps # </table>
(-> ph ps) , phps
impRemove1 # <title> Remove Implies </title> # <table> # [ ph ] # (<-> (-> [ ph ] ps) ps) # </table>
ph(<-> (-> ph ps) ps)
impRemove2 # <title> Remove Implies </title> # <table> # [ ph ] # (<-> (-> ps [ ph ] ) (T)) # </table>
ph(<-> (-> ps ph) (T))
impNotRemove1 # <title> Remove Implies </title> # <table> # [ (-. [ ph ] ) # (<-> (-> [ [ ph ] ps) (T)) # </table>
(-. ph)(<-> (-> ph ps) (T))
impNotRemove2 # <title> Remove Equivalence </title> # <table> # [ (-. [ ph ] ) # (<-> (-> ps [ [ ph ] ) (-. ps)) # </table>
(-. ph)(<-> (-> ps ph) (-. ps))
biRemove1 # <title> Remove Equivalence </title> # <table> # [ ph ] # (<-> (<-> [ ph ] ps) ps) # </table>
ph(<-> (<-> ph ps) ps)
biRemove2 # <title> Remove Equivalence </title> # <table> # [ ph ] # (<-> (<-> ps [ ph ] ) ps) # </table>
ph(<-> (<-> ps ph) ps)
biNotRemove2 # <title> Remove Equivalence </title> # <table> # [ (-. [ ph ] ) # (<-> (<-> ps [ [ ph ] ) (-. ps)) # </table>
(-. ph)(<-> (<-> ps ph) (-. ps))
biNotRemove1 # <title> Remove Equivalence </title> # <table> # [ (-. [ ph ] ) # (<-> (<-> [ [ ph ] ps) ps) # </table>
(-. ph)(<-> (<-> ph ps) (-. ps))
anRemove1 # <title> Remove AND </title> # <table> # [ ph ] # (<-> (/\ [ ph ] ps) ps) # </table>
ph(<-> (/\ ph ps) ps)
anRemove2 # <title> Remove AND </title> # <table> # [ ph ] # (<-> (/\ ps [ ph ] ) ps) # </table>
ph(<-> (/\ ps ph) ps)
anNotRemove1 # <title> Remove AND </title> # <table> # [ (-. [ ph ] ) # (<-> (/\ [ [ ph ] ps) (F)) # </table>
(-. ph)(<-> (/\ ph ps) (F))
anNotRemove2 # <title> Remove AND </title> # <table> # [ (-. [ ph ] ) # (<-> (/\ ps [ [ ph ] ) (F)) # </table>
(-. ph)(<-> (/\ ps ph) (F))
orRemove1 # <title> Remove OR </title> # <table> # [ ph ] # (<-> (\/ [ ph ] ps) (T)) # </table>
ph(<-> (\/ ph ps) (T))
orRemove2 # <title> Remove OR </title> # <table> # [ ph ] # (<-> (\/ ps [ ph ] ) (T)) # </table>
ph(<-> (\/ ps ph) (T))
orNotRemove1 # <title> Remove OR </title> # <table> # [ (-. [ ph ] ) # (<-> (\/ [ [ ph ] ps) ps) # </table>
(-. ph)(<-> (\/ ph ps) ps)
orNotRemove2 # <title> Remove OR </title> # <table> # [ (-. [ ph ] ) # (<-> (\/ ps [ [ ph ] ) ps) # </table>
(-. ph)(<-> (\/ ps ph) ps)
mpbiRemove mpbi with the order of the first and second hypotheses reversed. # <title> Modus Ponens </title> # <table> # (<-> ph ] [ ps ] ) # ph ] ] ] # [ [ ps ] # </table>
(<-> ph ps) , phps
mpbirRemove mpbir with the order of the first and second hypotheses reversed. # <title> Modus Ponens </title> # <table> # (<-> ph ] [ ps ] ) # [ [ ps ] # ph ] ] ] # </table>
(<-> ph ps) , psph
BiReplaceBi1Not0Imp1 # <title> Substitution </title> # <table> # (<-> ph (-. (-> ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (-. (-> ps [ [ [ th ] ))) # </table>
(<-> ph (-. (-> ps ch))) , (<-> ch th)(<-> ph (-. (-> ps th)))
BiReplaceBi1Imp0 # <title> Substitution </title> # <table> # (<-> ph (-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (<-> ph (-> [ [ [ ch ] th)) # </table>
(<-> ph (-> ps th)) , (<-> ps ch)(<-> ph (-> ch th))
biTrue # <title> A theorem is equivalent to True </title>
ps(<-> ps (T))
biFalse # <title> A falsehood is equivalent to False </title>
(-. ph)(<-> ph (F))
notT # <title> Truth Table for Negation </title>
(<-> (-. (T)) (F))
notF # <title> Truth Table for Negation </title>
(<-> (-. (F)) (T))
imTT # <title> Truth Table </title>
(<-> (-> (T) (T)) (T))
imFT # <title> Truth Table </title>
(<-> (-> (F) (T)) (T))
imTF # <title> Truth Table </title>
(<-> (-> (T) (F)) (F))
imFF # <title> Truth Table </title>
(<-> (-> (F) (F)) (T))
biTT # <title> Truth Table </title>
(<-> (<-> (T) (T)) (T))
biTF # <title> Truth Table </title>
(<-> (<-> (T) (F)) (F))
biFT # <title> Truth Table </title>
(<-> (<-> (F) (T)) (F))
biFF # <title> Truth Table </title>
(<-> (<-> (F) (F)) (T))
anTT # <title> Truth Table </title>
(<-> (/\ (T) (T)) (T))
anFF # <title> Truth Table </title>
(<-> (/\ (F) (F)) (F))
anTF # <title> Truth Table </title>
(<-> (/\ (T) (F)) (F))
anFT # <title> Truth Table </title>
(<-> (/\ (F) (T)) (F))
orTT # <title> Truth Table </title>
(<-> (\/ (T) (T)) (T))
orFF # <title> Truth Table </title>
(<-> (\/ (F) (F)) (F))
orTF # <title> Truth Table </title>
(<-> (\/ (T) (F)) (T))
orFT # <title> Truth Table </title>
(<-> (\/ (F) (T)) (T))
impRemoveT1 # <title> A true antecedent proves the consequent </title>
(<-> (-> (T) ps) ps)
impRemoveT2 # <title> A true consequent, proves the conditional </title>
(<-> (-> ps (T)) (T))
impRemoveF1 # <title> A false antecedent, proves the conditional </title>
(<-> (-> (F) ps) (T))
impRemoveF2 # <title> A false consequent, disproves the antecedent </title>
(<-> (-> ps (F)) (-. ps))
biRemoveT1 # <title> A truth affirms the biconditional </title>
(<-> (<-> (T) ps) ps)
biRemoveT2 # <title> A truth affirms the biconditional </title>
(<-> (<-> ps (T)) ps)
biRemoveF1 # <title> A falsehood negates the biconditional </title>
(<-> (<-> (F) ps) (-. ps))
biRemoveF2 # <title> A falsehood negates the biconditional </title>
(<-> (<-> ps (F)) (-. ps))
anRemoveT1 # <title> Remove truth from conjunction </title>
(<-> (/\ (T) ps) ps)
anRemoveT2 # <title> Remove truth from conjunction </title>
(<-> (/\ ps (T)) ps)
anRemoveF1 # <title> One falsehood makes a conjunction false </title>
(<-> (/\ (F) ps) (F))
anRemoveF2 # <title> One falsehood makes a conjunction false </title>
(<-> (/\ ps (F)) (F))
orRemoveT1 # <title> One truth makes a disjunction true </title>
(<-> (\/ (T) ps) (T))
orRemoveT2 # <title> One truth makes a disjunction true </title>
(<-> (\/ ps (T)) (T))
orRemoveF1 # <title> Remove falsehood from disjunction </title>
(<-> (\/ (F) ps) ps)
orRemoveF2 # <title> Remove falsehood from disjunction </title>
(<-> (\/ ps (F)) ps)
ImpReplaceBi1 # <title> Substitution </title> # <table> # (<-> ph [ ps ] ] ] ) # (-> [ ps ] [ ch ] ) # (<-> ph [ [ [ ch ] ) # </table>
(<-> ph ps) , (-> ps ch)(-> ph ch)
mpbi-inline # <suggest> right('Simplify', '↔') </suggest>
(-> (/\ ph (<-> ph ps)) ps)
(-> (/\ ph ps) ch)(-> ps (-> ph ch))
(-> (/\ ph (-> ps ch)) (-> ps (/\ ph ch)))