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	pm2.07 901	Theorem *2.07 of [WhiteheadRussell] p. 101. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 → (𝜑 ∨ 𝜑))
Theorem	pm1.2 902	Axiom *1.2 of [WhiteheadRussell] p. 96, which they call "Taut". (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜑) → 𝜑)
Theorem	oridm 903	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 904	Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∨ 𝜑))
Theorem	pm2.4 905	Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓))
Theorem	pm2.41 906	Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓))
Theorem	orim12i 907	Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))
Theorem	orim1i 908	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜒))
Theorem	orim2i 909	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))
Theorem	orim12dALT 910	Alternate proof of orim12d 965 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 911	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 912	Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))
Theorem	orbi12i 913	Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))
Theorem	orbi2d 914	Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))
Theorem	orbi1d 915	Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))
Theorem	orbi1 916	Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒)))
Theorem	orbi12d 917	Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 21-Jun-1993.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜏)))
Theorem	pm1.5 918	Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜓 ∨ (𝜑 ∨ 𝜒)))
Theorem	or12 919	Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ (𝜓 ∨ (𝜑 ∨ 𝜒)))
Theorem	orass 920	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 921	Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → ((𝜑 ∨ 𝜓) ∨ 𝜒))
Theorem	pm2.32 922	Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ (𝜓 ∨ 𝜒)))
Theorem	pm2.3 923	Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜑 ∨ (𝜒 ∨ 𝜓)))
Theorem	or32 924	A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜓))
Theorem	or4 925	Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜃)))
Theorem	or42 926	Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜃 ∨ 𝜓)))
Theorem	orordi 927	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜒)))
Theorem	orordir 928	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜒)))
Theorem	orimdi 929	Disjunction distributes over implication. (Contributed by Wolf Lammen, 5-Jan-2013.)
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) ↔ ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)))
Theorem	pm2.76 930	Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 → 𝜒)) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)))
Theorem	pm2.85 931	Theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)) → (𝜑 ∨ (𝜓 → 𝜒)))
Theorem	pm2.75 932	Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.)
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒)))
Theorem	pm4.78 933	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 934	A disjunction with a true formula is equivalent to that true formula. (Contributed by NM, 23-May-1999.)
⊢ (𝜑 → (𝜑 ↔ (𝜑 ∨ 𝜓)))
Theorem	biorf 935	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 936	A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012.)
⊢ (𝜑 → (𝜓 ↔ (¬ 𝜑 ∨ 𝜓)))
Theorem	biorfi 937	The dual of biorf 935 is not biantr 805 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 938	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 939	Obsolete proof of biorfri 938 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 940	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 941	Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜑 ∨ 𝜓) → 𝜓))
Theorem	pm2.64 942	Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜓) → ((𝜑 ∨ ¬ 𝜓) → 𝜑))
Theorem	pm2.42 943	Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∨ (𝜑 → 𝜓)) → (𝜑 → 𝜓))
Theorem	pm5.11g 944	A general instance of Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) ∨ (¬ 𝜑 → 𝜒))
Theorem	pm5.11 945	Theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) ∨ (¬ 𝜑 → 𝜓))
Theorem	pm5.12 946	Theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) ∨ (𝜑 → ¬ 𝜓))
Theorem	pm5.14 947	Theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) ∨ (𝜓 → 𝜒))
Theorem	pm5.13 948	Theorem *5.13 of [WhiteheadRussell] p. 123. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ ((𝜑 → 𝜓) ∨ (𝜓 → 𝜑))
Theorem	pm5.55 949	Theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 20-Jan-2013.)
⊢ (((𝜑 ∨ 𝜓) ↔ 𝜑) ∨ ((𝜑 ∨ 𝜓) ↔ 𝜓))
Theorem	pm4.72 950	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 951	Simplify an implication between implications. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Wolf Lammen, 3-Apr-2013.)
⊢ (((𝜓 → 𝜒) → (𝜑 → 𝜒)) ↔ (𝜑 → (𝜓 ∨ 𝜒)))
Theorem	oibabs 952	Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)
⊢ (((𝜑 ∨ 𝜓) → (𝜑 ↔ 𝜓)) ↔ (𝜑 ↔ 𝜓))
Theorem	orbidi 953	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 954	Disjunction distributes over the biconditional. Theorem *5.7 of [WhiteheadRussell] p. 125. This theorem is similar to orbidi 953. (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 965 versus orim12dALT 910). These theorems are mostly grouped at the beginning of this section. The family of theorems starting with animorl 978 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 955 and related theorems.
Theorem	jaao 955	Inference conjoining and disjoining the antecedents of two implications. (Contributed by NM, 30-Sep-1999.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∨ 𝜏) → 𝜒))
Theorem	jaoa 956	Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜒))    ⇒   ⊢ ((𝜑 ∨ 𝜃) → ((𝜓 ∧ 𝜏) → 𝜒))
Theorem	jaoian 957	Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜃 ∧ 𝜓) → 𝜒)    ⇒   ⊢ (((𝜑 ∨ 𝜃) ∧ 𝜓) → 𝜒)
Theorem	jaodan 958	Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    ⇒   ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
Theorem	mpjaodan 959	Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30435. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜃) → 𝜒)    &   ⊢ (𝜑 → (𝜓 ∨ 𝜃))    ⇒   ⊢ (𝜑 → 𝜒)
Theorem	pm3.44 960	Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) → ((𝜓 ∨ 𝜒) → 𝜑))
Theorem	jao 961	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 962	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 963	Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) ↔ ((𝜓 ∨ 𝜒) → 𝜑))
Theorem	pm3.48 964	Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)))
Theorem	orim12d 965	Disjoin antecedents and consequents in a deduction. See orim12dALT 910 for a proof which does not depend on df-an 396. (Contributed by NM, 10-May-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜏)))
Theorem	orim1d 966	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → (𝜒 ∨ 𝜃)))
Theorem	orim2d 967	Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))
Theorem	orim2 968	Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜑 ∨ 𝜒)))
Theorem	pm2.38 969	Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜒 ∨ 𝜑)))
Theorem	pm2.36 970	Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
⊢ ((𝜓 → 𝜒) → ((𝜑 ∨ 𝜓) → (𝜒 ∨ 𝜑)))
Theorem	pm2.37 971	Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
⊢ ((𝜓 → 𝜒) → ((𝜓 ∨ 𝜑) → (𝜑 ∨ 𝜒)))
Theorem	pm2.81 972	Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 → (𝜒 → 𝜃)) → ((𝜑 ∨ 𝜓) → ((𝜑 ∨ 𝜒) → (𝜑 ∨ 𝜃))))
Theorem	pm2.8 973	Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
⊢ ((𝜑 ∨ 𝜓) → ((¬ 𝜓 ∨ 𝜒) → (𝜑 ∨ 𝜒)))
Theorem	pm2.73 974	Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜓) → (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜓 ∨ 𝜒)))
Theorem	pm2.74 975	Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ ((𝜓 → 𝜑) → (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ 𝜒)))
Theorem	pm2.82 976	Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) → (((𝜑 ∨ ¬ 𝜒) ∨ 𝜃) → ((𝜑 ∨ 𝜓) ∨ 𝜃)))
Theorem	pm4.39 977	Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ↔ 𝜒) ∧ (𝜓 ↔ 𝜃)) → ((𝜑 ∨ 𝜓) ↔ (𝜒 ∨ 𝜃)))
Theorem	animorl 978	Conjunction implies disjunction with one common formula (1/4). (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∨ 𝜒))
Theorem	animorr 979	Conjunction implies disjunction with one common formula (2/4). (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∨ 𝜓))
Theorem	animorlr 980	Conjunction implies disjunction with one common formula (3/4). (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∨ 𝜑))
Theorem	animorrl 981	Conjunction implies disjunction with one common formula (4/4). (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒))
Theorem	ianor 982	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 983	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 984	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 985	Theorem *4.52 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.)
⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (¬ 𝜑 ∨ 𝜓))
Theorem	pm4.53 986	Theorem *4.53 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∧ ¬ 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
Theorem	pm4.54 987	Theorem *4.54 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.)
⊢ ((¬ 𝜑 ∧ 𝜓) ↔ ¬ (𝜑 ∨ ¬ 𝜓))
Theorem	pm4.55 988	Theorem *4.55 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 ∧ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))
Theorem	pm4.56 989	Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))
Theorem	oran 990	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 991	Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 ∧ ¬ 𝜓) ↔ (𝜑 ∨ 𝜓))
Theorem	pm3.1 992	Theorem *3.1 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∧ 𝜓) → ¬ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	pm3.11 993	Theorem *3.11 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 ∨ ¬ 𝜓) → (𝜑 ∧ 𝜓))
Theorem	pm3.12 994	Theorem *3.12 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓))
Theorem	pm3.13 995	Theorem *3.13 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	pm3.14 996	Theorem *3.14 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
Theorem	pm4.44 997	Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∨ (𝜑 ∧ 𝜓)))
Theorem	pm4.45 998	Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∧ (𝜑 ∨ 𝜓)))
Theorem	orabs 999	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.)
⊢ (𝜑 ↔ ((𝜑 ∨ 𝜓) ∧ 𝜑))
Theorem	oranabs 1000	Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.)
⊢ (((𝜑 ∨ ¬ 𝜓) ∧ 𝜓) ↔ (𝜑 ∧ 𝜓))