P. 10 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 901-1000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfor2 901	Logical 'or' expressed in terms of implication only. Theorem *5.25 of [WhiteheadRussell] p. 124. (Contributed by NM, 12-Aug-2004.) (Proof shortened by Wolf Lammen, 20-Oct-2012.)
⊢ ((𝜑 ∨ 𝜓) ↔ ((𝜑 → 𝜓) → 𝜓))
Theorem	pm2.07 902	Theorem *2.07 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 → (𝜑 ∨ 𝜑))
Theorem	pm1.2 903	Axiom *1.2 of [WhiteheadRussell] p. 96, which they call "Taut". (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜑) → 𝜑)
Theorem	oridm 904	Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.)
⊢ ((𝜑 ∨ 𝜑) ↔ 𝜑)
Theorem	pm4.25 905	Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∨ 𝜑))
Theorem	pm2.4 906	Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓))
Theorem	pm2.41 907	Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓))
Theorem	orim12i 908	Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))
Theorem	orim1i 909	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜒))
Theorem	orim2i 910	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))
Theorem	orim12dALT 911	Alternate proof of orim12d 966 which does not depend on df-an 396. This is an illustration of the conservativity of definitions (definitions do not permit to prove additional theorems whose statements do not contain the defined symbol). (Contributed by Wolf Lammen, 8-Aug-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
Theorem	orbi2i 912	Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))
Theorem	orbi1i 913	Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))
Theorem	orbi12i 914	Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))
Theorem	orbi2d 915	Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))
Theorem	orbi1d 916	Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))
Theorem	orbi1 917	Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)))
Theorem	orbi12d 918	Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
Theorem	pm1.5 919	Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜓 ∨ (𝜑 ∨ 𝜒)))
Theorem	or12 920	Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ (𝜓 ∨ (𝜑 ∨ 𝜒)))
Theorem	orass 921	Associative law for disjunction. Theorem *4.33 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
Theorem	pm2.31 922	Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → ((𝜑 ∨ 𝜓) ∨ 𝜒))
Theorem	pm2.32 923	Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ (𝜓 ∨ 𝜒)))
Theorem	pm2.3 924	Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜑 ∨ (𝜒 ∨ 𝜓)))
Theorem	or32 925	A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜓))
Theorem	or4 926	Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜃)))
Theorem	or42 927	Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜃 ∨ 𝜓)))
Theorem	orordi 928	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜒)))
Theorem	orordir 929	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜒)))
Theorem	orimdi 930	Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013.)
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) ↔ ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)))
Theorem	pm2.76 931	Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)))
Theorem	pm2.85 932	Theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)) → (𝜑 ∨ (𝜓 → 𝜒)))
Theorem	pm2.75 933	Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.)
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒)))
Theorem	pm4.78 934	Implication distributes over disjunction. Theorem *4.78 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
⊢ (((𝜑 → 𝜓) ∨ (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∨ 𝜒)))
Theorem	biort 935	A disjunction with a true formula is equivalent to that true formula. (Contributed by NM, 23-May-1999.)
⊢ (𝜑 → (𝜑 ↔ (𝜑 ∨ 𝜓)))
Theorem	biorf 936	A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [WhiteheadRussell] p. 121. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓)))
Theorem	biortn 937	A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012.)
⊢ (𝜑 → (𝜓 ↔ (¬ 𝜑 ∨ 𝜓)))
Theorem	biorfi 938	The dual of biorf 936 is not biantr 806 but iba 527 (and ibar 528). So there should also be a "biorfr". (Note that these four statements can actually be strengthened to biconditionals.) (Contributed by BJ, 26-Oct-2019.)
⊢ ¬ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜑 ∨ 𝜓))
Theorem	biorfri 939	A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 16-Jul-2021.) (Proof shortened by AV, 10-Aug-2025.)
⊢ ¬ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))
Theorem	biorfriOLD 940	Obsolete version of biorfri 939 as of 10-Aug-2025. A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 16-Jul-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ¬ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑))
Theorem	pm2.26 941	Theorem *2.26 of [WhiteheadRussell] p. 104. See pm2.27 42. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
⊢ (¬ 𝜑 ∨ ((𝜑 → 𝜓) → 𝜓))
Theorem	pm2.63 942	Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜑 ∨ 𝜓) → 𝜓))
Theorem	pm2.64 943	Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ ¬ 𝜓) → 𝜑))
Theorem	pm2.42 944	Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∨ (𝜑 → 𝜓)) → (𝜑 → 𝜓))
Theorem	pm5.11g 945	A general instance of Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) ∨ (¬ 𝜑 → 𝜒))
Theorem	pm5.11 946	Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) ∨ (¬ 𝜑 → 𝜓))
Theorem	pm5.12 947	Theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) ∨ (𝜑 → ¬ 𝜓))
Theorem	pm5.14 948	Theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) ∨ (𝜓 → 𝜒))
Theorem	pm5.13 949	Theorem *5.13 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ ((𝜑 → 𝜓) ∨ (𝜓 → 𝜑))
Theorem	pm5.55 950	Theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 20-Jan-2013.)
⊢ (((𝜑 ∨ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∨ 𝜓) ↔ 𝜓))
Theorem	pm4.72 951	Implication in terms of biconditional and disjunction. Theorem *4.72 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jan-2013.)
⊢ ((𝜑 → 𝜓) ↔ (𝜓 ↔ (𝜑 ∨ 𝜓)))
Theorem	imimorb 952	Simplify an implication between implications. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)
⊢ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∨ 𝜒)))
Theorem	oibabs 953	Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓)) ↔ (𝜑 ↔ 𝜓))
Theorem	orbidi 954	Disjunction distributes over the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs" (1998), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.3384. (Contributed by NM, 8-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Feb-2013.)
⊢ ((𝜑 ∨ (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ↔ (𝜑 ∨ 𝜒)))
Theorem	pm5.7 955	Disjunction distributes over the biconditional. Theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbidi 954. (Contributed by Roy F. Longton, 21-Jun-2005.)
⊢ (((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)) ↔ (𝜒 ∨ (𝜑 ↔ 𝜓)))
1.2.8  Mixed connectives This section gathers theorems of propositional calculus which use (either in their statement or proof) mixed connectives (at least conjunction and disjunction). As noted in the "note on definitions" in the section comment for logical equivalence, some theorem statements may contain for instance only conjunction or only disjunction, but both definitions are used in their proofs to make them shorter (this is exemplified in orim12d 966 versus orim12dALT 911). These theorems are mostly grouped at the beginning of this section. The family of theorems starting with animorl 979 focus on the relation between conjunction and disjunction and can be seen as the starting point of mixed connectives in statements. This sectioning is not rigorously true, since for instance the section begins with jaao 956 and related theorems.
Theorem	jaao 956	Inference conjoining and disjoining the antecedents of two implications. (Contributed by NM, 30-Sep-1999.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∨ 𝜏) → 𝜒))
Theorem	jaoa 957	Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜒))    ⇒   ⊢ ((𝜑 ∨ 𝜃) → ((𝜓 ∧ 𝜏) → 𝜒))
Theorem	jaoian 958	Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒)
Theorem	jaodan 959	Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
Theorem	mpjaodan 960	Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30431. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm3.44 961	Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) → ((𝜓 ∨ 𝜒) → 𝜑))
Theorem	jao 962	Disjunction of antecedents. Compare Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 4-Apr-2013.)
⊢ ((𝜑 → 𝜓) → ((𝜒 → 𝜓) → ((𝜑 ∨ 𝜒) → 𝜓)))
Theorem	jaob 963	Disjunction of antecedents. Compare Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-May-1994.) (Proof shortened by Wolf Lammen, 9-Dec-2012.)
⊢ (((𝜑 ∨ 𝜒) → 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓)))
Theorem	pm4.77 964	Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) ↔ ((𝜓 ∨ 𝜒) → 𝜑))
Theorem	pm3.48 965	Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)))
Theorem	orim12d 966	Disjoin antecedents and consequents in a deduction. See orim12dALT 911 for a proof which does not depend on df-an 396. (Contributed by NM, 10-May-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
Theorem	orim1d 967	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃)))
Theorem	orim2d 968	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))
Theorem	orim2 969	Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)))
Theorem	pm2.38 970	Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜒 ∨ 𝜑)))
Theorem	pm2.36 971	Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜒 ∨ 𝜑)))
Theorem	pm2.37 972	Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜒)))
Theorem	pm2.81 973	Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 → (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜓) → ((𝜑 ∨ 𝜒) → (𝜑 ∨ 𝜃))))
Theorem	pm2.8 974	Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜒)))
Theorem	pm2.73 975	Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) → (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜓 ∨ 𝜒)))
Theorem	pm2.74 976	Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ ((𝜓 → 𝜑) → (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ 𝜒)))
Theorem	pm2.82 977	Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) → (((𝜑 ∨ ¬ 𝜒) ∨ 𝜃) → ((𝜑 ∨ 𝜓) ∨ 𝜃)))
Theorem	pm4.39 978	Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ↔ 𝜒) ∧ (𝜓 ↔ 𝜃)) → ((𝜑 ∨ 𝜓) ↔ (𝜒 ∨ 𝜃)))
Theorem	animorl 979	Conjunction implies disjunction with one common formula (1/4). (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∨ 𝜒))
Theorem	animorr 980	Conjunction implies disjunction with one common formula (2/4). (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∨ 𝜓))
Theorem	animorlr 981	Conjunction implies disjunction with one common formula (3/4). (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∨ 𝜑))
Theorem	animorrl 982	Conjunction implies disjunction with one common formula (4/4). (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒))
Theorem	ianor 983	Negated conjunction in terms of disjunction (De Morgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	anor 984	Conjunction in terms of disjunction (De Morgan's law). Theorem *4.5 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 3-Nov-2012.)
⊢ ((𝜑 ∧ 𝜓) ↔ ¬ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	ioran 985	Negated disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (¬ (𝜑 ∨ 𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
Theorem	pm4.52 986	Theorem *4.52 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.)
⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (¬ 𝜑 ∨ 𝜓))
Theorem	pm4.53 987	Theorem *4.53 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∧ ¬ 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
Theorem	pm4.54 988	Theorem *4.54 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.)
⊢ ((¬ 𝜑 ∧ 𝜓) ↔ ¬ (𝜑 ∨ ¬ 𝜓))
Theorem	pm4.55 989	Theorem *4.55 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 ∧ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))
Theorem	pm4.56 990	Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))
Theorem	oran 991	Disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ ((𝜑 ∨ 𝜓) ↔ ¬ (¬ 𝜑 ∧ ¬ 𝜓))
Theorem	pm4.57 992	Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 ∧ ¬ 𝜓) ↔ (𝜑 ∨ 𝜓))
Theorem	pm3.1 993	Theorem *3.1 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∧ 𝜓) → ¬ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	pm3.11 994	Theorem *3.11 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 ∨ ¬ 𝜓) → (𝜑 ∧ 𝜓))
Theorem	pm3.12 995	Theorem *3.12 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓))
Theorem	pm3.13 996	Theorem *3.13 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	pm3.14 997	Theorem *3.14 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
Theorem	pm4.44 998	Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∨ (𝜑 ∧ 𝜓)))
Theorem	pm4.45 999	Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∧ (𝜑 ∨ 𝜓)))
Theorem	orabs 1000	Absorption of redundant internal disjunct. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 28-Feb-2014.)
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ 𝜑))