P. 6 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 501-600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	biimpar 501	Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
Theorem	biimpac 502	Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜓 ∧ 𝜑) → 𝜒)
Theorem	biimparc 503	Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
Theorem	animorl 504	Conjunction implies disjunction with one common formula (1/4). (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∨ 𝜒))
Theorem	animorr 505	Conjunction implies disjunction with one common formula (2/4). (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∨ 𝜓))
Theorem	animorlr 506	Conjunction implies disjunction with one common formula (3/4). (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ∧ 𝜓) → (𝜒 ∨ 𝜑))
Theorem	animorrl 507	Conjunction implies disjunction with one common formula (4/4). (Contributed by BJ, 4-Oct-2019.)
⊢ ((𝜑 ∧ 𝜓) → (𝜓 ∨ 𝜒))
Theorem	ianor 508	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 509	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 510	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 511	Theorem *4.52 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.)
⊢ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (¬ 𝜑 ∨ 𝜓))
Theorem	pm4.53 512	Theorem *4.53 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∧ ¬ 𝜓) ↔ (¬ 𝜑 ∨ 𝜓))
Theorem	pm4.54 513	Theorem *4.54 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 5-Nov-2012.)
⊢ ((¬ 𝜑 ∧ 𝜓) ↔ ¬ (𝜑 ∨ ¬ 𝜓))
Theorem	pm4.55 514	Theorem *4.55 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 ∧ 𝜓) ↔ (𝜑 ∨ ¬ 𝜓))
Theorem	pm4.56 515	Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 ∨ 𝜓))
Theorem	oran 516	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 517	Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 ∧ ¬ 𝜓) ↔ (𝜑 ∨ 𝜓))
Theorem	pm3.1 518	Theorem *3.1 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∧ 𝜓) → ¬ (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	pm3.11 519	Theorem *3.11 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (¬ 𝜑 ∨ ¬ 𝜓) → (𝜑 ∧ 𝜓))
Theorem	pm3.12 520	Theorem *3.12 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) ∨ (𝜑 ∧ 𝜓))
Theorem	pm3.13 521	Theorem *3.13 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ (¬ (𝜑 ∧ 𝜓) → (¬ 𝜑 ∨ ¬ 𝜓))
Theorem	pm3.14 522	Theorem *3.14 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))
Theorem	iba 523	Introduction of antecedent as conjunct. Theorem *4.73 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Mar-1994.)
⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑)))
Theorem	ibar 524	Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.)
⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓)))
Theorem	biantru 525	A wff is equivalent to its conjunction with truth. (Contributed by NM, 26-May-1993.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑))
Theorem	biantrur 526	A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)
⊢ 𝜑    ⇒   ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓))
Theorem	biantrud 527	A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ↔ (𝜒 ∧ 𝜓)))
Theorem	biantrurd 528	A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒)))
Theorem	mpbirand 529	Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 ↔ 𝜃))
Theorem	jaao 530	Inference conjoining and disjoining the antecedents of two implications. (Contributed by NM, 30-Sep-1999.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → ((𝜓 ∨ 𝜏) → 𝜒))
Theorem	jaoa 531	Inference disjoining and conjoining the antecedents of two implications. (Contributed by Stefan Allan, 1-Nov-2008.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜏 → 𝜒))    ⇒   ⊢ ((𝜑 ∨ 𝜃) → ((𝜓 ∧ 𝜏) → 𝜒))
Theorem	pm3.44 532	Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)
⊢ (((𝜓 → 𝜑) ∧ (𝜒 → 𝜑)) → ((𝜓 ∨ 𝜒) → 𝜑))
Theorem	jao 533	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	pm1.2 534	Axiom *1.2 of [WhiteheadRussell] p. 96, which they call "Taut". (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ 𝜑) → 𝜑)
Theorem	oridm 535	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 536	Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∨ 𝜑))
Theorem	orim12i 537	Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃))
Theorem	orim1i 538	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜒))
Theorem	orim2i 539	Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))
Theorem	orbi2i 540	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 541	Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))
Theorem	orbi12i 542	Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 ↔ 𝜓)    &   ⊢ (𝜒 ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))
Theorem	pm1.5 543	Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜓 ∨ (𝜑 ∨ 𝜒)))
Theorem	or12 544	Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ (𝜓 ∨ (𝜑 ∨ 𝜒)))
Theorem	orass 545	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 546	Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → ((𝜑 ∨ 𝜓) ∨ 𝜒))
Theorem	pm2.32 547	Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) → (𝜑 ∨ (𝜓 ∨ 𝜒)))
Theorem	or32 548	A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ 𝜓))
Theorem	or4 549	Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜃)))
Theorem	or42 550	Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
⊢ (((𝜑 ∨ 𝜓) ∨ (𝜒 ∨ 𝜃)) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜃 ∨ 𝜓)))
Theorem	orordi 551	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∨ 𝜓) ∨ (𝜑 ∨ 𝜒)))
Theorem	orordir 552	Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
⊢ (((𝜑 ∨ 𝜓) ∨ 𝜒) ↔ ((𝜑 ∨ 𝜒) ∨ (𝜓 ∨ 𝜒)))
Theorem	jca 553	Deduce conjunction of the consequents of two implications ("join consequents with 'and'"). Equivalent to the natural deduction rule ∧ I (∧ introduction), see natded 26652. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒))
Theorem	jcad 554	Deduction conjoining the consequents of two implications. (Contributed by NM, 15-Jul-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))
Theorem	jca31 555	Join three consequents. (Contributed by Jeff Hankins, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
Theorem	jca32 556	Join three consequents. (Contributed by FL, 1-Aug-2009.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 ∧ (𝜒 ∧ 𝜃)))
Theorem	jcai 557	Deduction replacing implication with conjunction. (Contributed by NM, 15-Jul-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒))
Theorem	jctil 558	Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    ⇒   ⊢ (𝜑 → (𝜒 ∧ 𝜓))
Theorem	jctir 559	Inference conjoining a theorem to right of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
⊢ (𝜑 → 𝜓)    &   ⊢ 𝜒    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒))
Theorem	jccir 560	Inference conjoining a consequent of a consequent to the right of the consequent in an implication. See also ex-natded5.3i 26658. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by AV, 20-Aug-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜒))
Theorem	jccil 561	Inference conjoining a consequent of a consequent to the left of the consequent in an implication. Remark: One can also prove this theorem using syl 17 and jca 553 (as done in jccir 560), which would be 4 bytes shorter, but one step longer than the current proof. (Proof modification is discouraged.) (Contributed by AV, 20-Aug-2019.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ (𝜑 → (𝜒 ∧ 𝜓))
Theorem	jctl 562	Inference conjoining a theorem to the left of a consequent. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.)
⊢ 𝜓    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜑))
Theorem	jctr 563	Inference conjoining a theorem to the right of a consequent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.)
⊢ 𝜓    ⇒   ⊢ (𝜑 → (𝜑 ∧ 𝜓))
Theorem	jctild 564	Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))
Theorem	jctird 565	Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))
Theorem	syl6an 566	A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ ((𝜓 ∧ 𝜃) → 𝜏)    ⇒   ⊢ (𝜑 → (𝜒 → 𝜏))
Theorem	ancl 567	Conjoin antecedent to left of consequent. (Contributed by NM, 15-Aug-1994.)
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜑 ∧ 𝜓)))
Theorem	anclb 568	Conjoin antecedent to left of consequent. Theorem *4.7 of [WhiteheadRussell] p. 120. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜑 ∧ 𝜓)))
Theorem	pm5.42 569	Theorem *5.42 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → (𝜓 → 𝜒)) ↔ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒))))
Theorem	ancr 570	Conjoin antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
⊢ ((𝜑 → 𝜓) → (𝜑 → (𝜓 ∧ 𝜑)))
Theorem	ancrb 571	Conjoin antecedent to right of consequent. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)
⊢ ((𝜑 → 𝜓) ↔ (𝜑 → (𝜓 ∧ 𝜑)))
Theorem	ancli 572	Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜑 ∧ 𝜓))
Theorem	ancri 573	Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (𝜑 → (𝜓 ∧ 𝜑))
Theorem	ancld 574	Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜓 ∧ 𝜒)))
Theorem	ancrd 575	Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓)))
Theorem	anc2l 576	Conjoin antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 14-Jul-2013.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜑 ∧ 𝜒))))
Theorem	anc2r 577	Conjoin antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.)
⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜑 → (𝜓 → (𝜒 ∧ 𝜑))))
Theorem	anc2li 578	Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 10-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜒)))
Theorem	anc2ri 579	Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜑)))
Theorem	pm3.41 580	Theorem *3.41 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 → 𝜒) → ((𝜑 ∧ 𝜓) → 𝜒))
Theorem	pm3.42 581	Theorem *3.42 of [WhiteheadRussell] p. 113. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 → 𝜒) → ((𝜑 ∧ 𝜓) → 𝜒))
Theorem	pm3.4 582	Conjunction implies implication. Theorem *3.4 of [WhiteheadRussell] p. 113. (Contributed by NM, 31-Jul-1995.)
⊢ ((𝜑 ∧ 𝜓) → (𝜑 → 𝜓))
Theorem	pm4.45im 583	Conjunction with implication. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 17-May-1998.)
⊢ (𝜑 ↔ (𝜑 ∧ (𝜓 → 𝜑)))
Theorem	anim12d 584	Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜃 → 𝜏))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))
Theorem	anim12d1 585	Variant of anim12d 584 where the second implication does not depend on the antecedent. (Contributed by Rodolfo Medina, 12-Oct-2010.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → 𝜏)    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏)))
Theorem	anim1d 586	Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃)))
Theorem	anim2d 587	Add a conjunct to left of antecedent and consequent in a deduction. (Contributed by NM, 14-May-1993.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → ((𝜃 ∧ 𝜓) → (𝜃 ∧ 𝜒)))
Theorem	anim12i 588	Conjoin antecedents and consequents of two premises. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))
Theorem	anim12ci 589	Variant of anim12i 588 with commutation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜒 → 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜃 ∧ 𝜓))
Theorem	anim1i 590	Introduce conjunct to both sides of an implication. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜒))
Theorem	anim2i 591	Introduce conjunct to both sides of an implication. (Contributed by NM, 3-Jan-1993.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ ((𝜒 ∧ 𝜑) → (𝜒 ∧ 𝜓))
Theorem	anim12ii 592	Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007.) (Proof shortened by Wolf Lammen, 19-Jul-2013.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜃 → (𝜓 → 𝜏))    ⇒   ⊢ ((𝜑 ∧ 𝜃) → (𝜓 → (𝜒 ∧ 𝜏)))
Theorem	prth 593	Conjoin antecedents and consequents of two premises. This is the closed theorem form of anim12d 584. Theorem *3.47 of [WhiteheadRussell] p. 113. It was proved by Leibniz, and it evidently pleased him enough to call it praeclarum theorema (splendid theorem). (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜃)) → ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃)))
Theorem	pm2.3 594	Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) → (𝜑 ∨ (𝜒 ∨ 𝜓)))
Theorem	pm2.41 595	Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜓 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓))
Theorem	pm2.42 596	Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((¬ 𝜑 ∨ (𝜑 → 𝜓)) → (𝜑 → 𝜓))
Theorem	pm2.4 597	Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
⊢ ((𝜑 ∨ (𝜑 ∨ 𝜓)) → (𝜑 ∨ 𝜓))
Theorem	pm2.65da 598	Deduction rule for proof by contradiction. (Contributed by NM, 12-Jun-2014.)
⊢ ((𝜑 ∧ 𝜓) → 𝜒)    &   ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝜒)    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	pm4.44 599	Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
⊢ (𝜑 ↔ (𝜑 ∨ (𝜑 ∧ 𝜓)))
Theorem	pm4.14 600	Theorem *4.14 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 23-Oct-2012.)
⊢ (((𝜑 ∧ 𝜓) → 𝜒) ↔ ((𝜑 ∧ ¬ 𝜒) → ¬ 𝜓))