P. 451 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

pm14.123c 45001*

Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)

⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑)))

Theorem

pm14.18 45002

Theorem *14.18 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)

⊢ (∃!𝑥𝜑 → (∀𝑥𝜓 → [(℩𝑥𝜑) / 𝑥]𝜓))

Theorem

iotaequ 45003*

Theorem *14.2 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)

⊢ (℩𝑥𝑥 = 𝑦) = 𝑦

Theorem

iotavalb 45004*

Theorem *14.202 in [WhiteheadRussell] p. 189. A biconditional version of iotaval 6499. (Contributed by Andrew Salmon, 11-Jul-2011.)

⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (℩𝑥𝜑) = 𝑦))

Theorem

iotasbc5 45005*

Theorem *14.205 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 11-Jul-2011.)

⊢ (∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑦]𝜓 ↔ ∃𝑦(𝑦 = (℩𝑥𝜑) ∧ 𝜓)))

Theorem

pm14.24 45006*

Theorem *14.24 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)

⊢ (∃!𝑥𝜑 → ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = (℩𝑥𝜑)))

Theorem

iotavalsb 45007*

Theorem *14.242 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)

⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ([𝑦 / 𝑧]𝜓 ↔ [(℩𝑥𝜑) / 𝑧]𝜓))

Theorem

sbiota1 45008

Theorem *14.25 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)

⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓))

Theorem

sbaniota 45009

Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)

⊢ (∃!𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓))

Theorem

iotasbcq 45010

Theorem *14.272 in [WhiteheadRussell] p. 193. (Contributed by Andrew Salmon, 11-Jul-2011.)

⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([(℩𝑥𝜑) / 𝑦]𝜒 ↔ [(℩𝑥𝜓) / 𝑦]𝜒))

21.40.5  Set Theory

Theorem

elnev 45011*

Any set that contains one element less than the universe is not equal to it. (Contributed by Andrew Salmon, 16-Jun-2011.)

⊢ (𝐴 ∈ V ↔ {𝑥 ∣ ¬ 𝑥 = 𝐴} ≠ V)

Theorem

rusbcALT 45012

A version of Russell's paradox which is proven using proper substitution. (Contributed by Andrew Salmon, 18-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ {𝑥 ∣ 𝑥 ∉ 𝑥} ∉ V

Theorem

compeq 45013*

Equality between two ways of saying "the complement of 𝐴". (Contributed by Andrew Salmon, 15-Jul-2011.)

⊢ (V ∖ 𝐴) = {𝑥 ∣ ¬ 𝑥 ∈ 𝐴}

Theorem

compne 45014

The complement of 𝐴 is not equal to 𝐴. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 11-Nov-2021.)

⊢ (V ∖ 𝐴) ≠ 𝐴

Theorem

compab 45015

Two ways of saying "the complement of a class abstraction". (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by Mario Carneiro, 11-Dec-2016.)

⊢ (V ∖ {𝑧 ∣ 𝜑}) = {𝑧 ∣ ¬ 𝜑}

Theorem

conss2 45016

Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)

⊢ (𝐴 ⊆ (V ∖ 𝐵) ↔ 𝐵 ⊆ (V ∖ 𝐴))

Theorem

conss1 45017

Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)

⊢ ((V ∖ 𝐴) ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ 𝐴)

Theorem

ralbidar 45018

More general form of ralbida 3276. (Contributed by Andrew Salmon, 25-Jul-2011.)

⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))

Theorem

rexbidar 45019

More general form of rexbida 3277. (Contributed by Andrew Salmon, 25-Jul-2011.)

⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))

Theorem

dropab1 45020

Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)

⊢ (∀𝑥 𝑥 = 𝑦 → {⟨𝑥, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ 𝜑})

Theorem

dropab2 45021

Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)

⊢ (∀𝑥 𝑥 = 𝑦 → {⟨𝑧, 𝑥⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜑})

Theorem

ipo0 45022

If the identity relation partially orders any class, then that class is the null class. (Contributed by Andrew Salmon, 25-Jul-2011.)

⊢ ( I Po 𝐴 ↔ 𝐴 = ∅)

Theorem

ifr0 45023

A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011.)

⊢ ( I Fr 𝐴 ↔ 𝐴 = ∅)

Theorem

ordpss 45024

ordelpss 6378 with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011.)

⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → 𝐴 ⊊ 𝐵))

Theorem

fvsb 45025*

Explicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)

⊢ (∃!𝑦 𝐴𝐹𝑦 → ([(𝐹‘𝐴) / 𝑥]𝜑 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑)))

Theorem

fveqsb 45026*

Implicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)

⊢ (𝑥 = (𝐹‘𝐴) → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃!𝑦 𝐴𝐹𝑦 → (𝜓 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑)))

Theorem

xpexb 45027

A Cartesian product exists iff its converse does. Corollary 6.9(1) in [TakeutiZaring] p. 26. (Contributed by Andrew Salmon, 13-Nov-2011.)

⊢ ((𝐴 × 𝐵) ∈ V ↔ (𝐵 × 𝐴) ∈ V)

Theorem

trelpss 45028

An element of a transitive set is a proper subset of it. Theorem 7.2 in [TakeutiZaring] p. 35. Unlike tz7.2 5635, ax-reg 9542 is required for its proof. (Contributed by Andrew Salmon, 13-Nov-2011.)

⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊊ 𝐴)

21.40.6  Arithmetic

Theorem

addcomgi 45029

Generalization of commutative law for addition. Simplifies proofs dealing with vectors. However, it is dependent on our particular definition of ordered pair. (Contributed by Andrew Salmon, 28-Jan-2012.) (Revised by Mario Carneiro, 6-May-2015.)

⊢ (𝐴 + 𝐵) = (𝐵 + 𝐴)

21.40.7  Geometry

Syntax

cplusr 45030

Introduce the operation of vector addition.

class +_𝑟

Syntax

cminusr 45031

Introduce the operation of vector subtraction.

class -_𝑟

Syntax

ctimesr 45032

Introduce the operation of scalar multiplication.

class ._𝑣

Syntax

cptdfc 45033

PtDf is a predicate that is crucial for the definition of lines as well as proving a number of important theorems.

class PtDf(𝐴, 𝐵)

Syntax

crr3c 45034

RR3 is a class.

class RR3

Syntax

cline3 45035

line3 is a class.

class line3

Definition

df-addr 45036*

Define the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ +_𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) + (𝑦‘𝑣))))

Definition

df-subr 45037*

Define the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ -_𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) − (𝑦‘𝑣))))

Definition

df-mulv 45038*

Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ._𝑣 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ (𝑥 · (𝑦‘𝑣))))

Theorem

addrval 45039*

Value of the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+_𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) + (𝐵‘𝑣))))

Theorem

subrval 45040*

Value of the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-_𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) − (𝐵‘𝑣))))

Theorem

mulvval 45041*

Value of the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴._𝑣𝐵) = (𝑣 ∈ ℝ ↦ (𝐴 · (𝐵‘𝑣))))

Theorem

addrfv 45042

Vector addition at a value. The operation takes each vector 𝐴 and 𝐵 and forms a new vector whose values are the sum of each of the values of 𝐴 and 𝐵. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴+_𝑟𝐵)‘𝐶) = ((𝐴‘𝐶) + (𝐵‘𝐶)))

Theorem

subrfv 45043

Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴-_𝑟𝐵)‘𝐶) = ((𝐴‘𝐶) − (𝐵‘𝐶)))

Theorem

mulvfv 45044

Scalar multiplication at a value. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴._𝑣𝐵)‘𝐶) = (𝐴 · (𝐵‘𝐶)))

Theorem

addrfn 45045

Vector addition produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+_𝑟𝐵) Fn ℝ)

Theorem

subrfn 45046

Vector subtraction produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-_𝑟𝐵) Fn ℝ)

Theorem

mulvfn 45047

Scalar multiplication producees a function. (Contributed by Andrew Salmon, 27-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴._𝑣𝐵) Fn ℝ)

Theorem

addrcom 45048

Vector addition is commutative. (Contributed by Andrew Salmon, 28-Jan-2012.)

⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+_𝑟𝐵) = (𝐵+_𝑟𝐴))

Definition

df-ptdf 45049*

Define the predicate PtDf, which is a utility definition used to shorten definitions and simplify proofs. (Contributed by Andrew Salmon, 15-Jul-2012.)

⊢ PtDf(𝐴, 𝐵) = (𝑥 ∈ ℝ ↦ (((𝑥._𝑣(𝐵-_𝑟𝐴)) +_𝑣 𝐴) “ {1, 2, 3}))

Definition

df-rr3 45050

Define the set of all points RR3. We define each point 𝐴 as a function to allow the use of vector addition and subtraction as well as scalar multiplication in our proofs. (Contributed by Andrew Salmon, 15-Jul-2012.)

⊢ RR3 = (ℝ ↑_m {1, 2, 3})

Definition

df-line3 45051*

Define the set of all lines. A line is an infinite subset of RR3 that satisfies a PtDf property. (Contributed by Andrew Salmon, 15-Jul-2012.)

⊢ line3 = {𝑥 ∈ 𝒫 RR3 ∣ (2_o ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → ran PtDf(𝑦, 𝑧) = 𝑥))}

21.41  Mathbox for Alan Sare

We are sad to report the passing of long-time contributor Alan Sare (Nov. 9, 1954 - Mar. 23, 2019).

Alan's first contribution to Metamath was a shorter proof for tfrlem8 8359 in 2008.

He developed a tool called "completeusersproof" that assists developing proofs using his "virtual deduction" method: https://us.metamath.org/other.html#completeusersproof 8359. His virtual deduction method is explained in the comment for wvd1 45143.

Below are some excerpts from his first emails to NM in 2007:

...I have been interested in proving set theory theorems for many years for mental exercise. I enjoy it. I have used a book by Martin Zuckerman. It is informal. I am interested in completely and perfectly proving theorems. Mr. Zuckerman leaves out most of the steps of a proof, of course, like most authors do, as you have noted. A complete proof for higher theorems would require a volume of writing similar to the Metamath documents. So I am frustrated when I am not capable of constructing a proof and Zuckerman leaves out steps I do not understand. I could search for the steps in other texts, but I don't do that too much. Metamath may be the answer for me....

...If we go beyond mathematics, I believe that it is possible to write down all human knowledge in a way similar to the way you have explicated large areas of mathematics. Of course, that would be a much, much more difficult job. For example, it is possible to take a hard science like physics, construct axioms based on experimental results, and to cast all of physics into a collection of axioms and theorems. Maybe this has already been attempted, although I am not familiar with it. When one then moves on to the soft sciences such as social science, this job gets much more difficult. The key is: All human thought consists of logical operations on abstract objects. Usually, these logical operations are done informally. There is no reason why one cannot take any subject and explicate it and take it down to the indivisible postulates in a formal rigorous way....

...When I read a math book or an engineering book I come across something I don't understand and I am compelled to understand it. But, often it is hopeless. I don't have the time. Or, I would have to read the same thing by multiple authors in the hope that different authors would give parts of the working proof that others have omitted. It is very inefficient. Because I have always been inclined to "get to the bottom" for a 100% fully understood proof....

21.41.1  Auxiliary theorems for the Virtual Deduction tool

Theorem

idiALT 45052

Placeholder for idi 1. Though unnecessary, this theorem is sometimes used in proofs in this mathbox for pedagogical purposes. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝜑    ⇒   ⊢ 𝜑

Theorem

exbir 45053

Exportation implication also converting the consequent from a biconditional to an implication. Derived automatically from exbirVD 45426. (Contributed by Alan Sare, 31-Dec-2011.)

⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜃 → 𝜒))))

Theorem

3impexpbicom 45054

Version of 3impexp 1375 where in addition the consequent is commuted. (Contributed by Alan Sare, 31-Dec-2011.)

⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))

Theorem

3impexpbicomi 45055

Inference associated with 3impexpbicom 45054. Derived automatically from 3impexpbicomiVD 45431. (Contributed by Alan Sare, 31-Dec-2011.)

⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))

21.41.2  Supplementary unification deductions

Theorem

bi1imp 45056

Importation inference similar to imp 411, except the outermost implication of the hypothesis is a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ (𝜑 ↔ (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

bi2imp 45057

Importation inference similar to imp 411, except both implications of the hypothesis are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ (𝜑 ↔ (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Theorem

bi3impb 45058

Similar to 3impb 1130 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

bi3impa 45059

Similar to 3impa 1125 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

bi23impib 45060

3impib 1132 with the inner implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

bi13impib 45061

3impib 1132 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ (𝜑 ↔ ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

bi123impib 45062

3impib 1132 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ (𝜑 ↔ ((𝜓 ∧ 𝜒) ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

bi13impia 45063

3impia 1133 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ ((𝜑 ∧ 𝜓) ↔ (𝜒 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

bi123impia 45064

3impia 1133 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ ((𝜑 ∧ 𝜓) ↔ (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

bi33imp12 45065

3imp 1126 with innermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

bi13imp23 45066

3imp 1126 with outermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ (𝜑 ↔ (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

bi13imp2 45067

Similar to 3imp 1126 except the outermost and innermost implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ (𝜑 ↔ (𝜓 → (𝜒 ↔ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

bi12imp3 45068

Similar to 3imp 1126 except all but innermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ (𝜑 ↔ (𝜓 ↔ (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

bi23imp1 45069

Similar to 3imp 1126 except all but outermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ (𝜑 → (𝜓 ↔ (𝜒 ↔ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

bi123imp0 45070

Similar to 3imp 1126 except all implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)

⊢ (𝜑 ↔ (𝜓 ↔ (𝜒 ↔ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Theorem

4animp1 45071

A single hypothesis unification deduction with an assertion which is an implication with a 4-right-nested conjunction antecedent. (Contributed by Alan Sare, 30-May-2018.)

⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜏 ↔ 𝜃))    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Theorem

4an31 45072

A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.)

⊢ ((((𝜒 ∧ 𝜓) ∧ 𝜑) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Theorem

4an4132 45073

A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.)

⊢ ((((𝜃 ∧ 𝜒) ∧ 𝜓) ∧ 𝜑) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)

Theorem

expcomdg 45074

Biconditional form of expcomd 421. (Contributed by Alan Sare, 22-Jul-2012.) (New usage is discouraged.)

⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜑 → (𝜒 → (𝜓 → 𝜃))))

21.41.3  Conventional Metamath proofs, some derived from VD proofs

Theorem

iidn3 45075

idn3 45189 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 23-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜒)))

Theorem

ee222 45076

e222 45210 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 7-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → 𝜃))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜒 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜓 → 𝜂))

Theorem

ee3bir 45077

Right-biconditional form of e3 45310 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 22-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜏 ↔ 𝜃)    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))

Theorem

ee13 45078

e13 45321 without virtual deduction connectives. Special theorem needed for the Virtual Deduction translation tool. (Contributed by Alan Sare, 28-Oct-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏)))    &   ⊢ (𝜓 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂)))

Theorem

ee121 45079

e121 45230 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜂))

Theorem

ee122 45080

e122 45227 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → 𝜏))    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜂))

Theorem

ee333 45081

e333 45306 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))    &   ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜁)))

Theorem

ee323 45082

e323 45339 without virtual deductions. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))    &   ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜁)))

Theorem

3ornot23 45083

If the second and third disjuncts of a true triple disjunction are false, then the first disjunct is true. Automatically derived from 3ornot23VD 45420. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒))

Theorem

orbi1r 45084

orbi1 930 with order of disjuncts reversed. Derived from orbi1rVD 45421. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)))

Theorem

3orbi123 45085

pm4.39 992 with a 3-conjunct antecedent. This proof is 3orbi123VD 45423 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (((𝜑 ↔ 𝜓) ∧ (𝜒 ↔ 𝜃) ∧ (𝜏 ↔ 𝜂)) → ((𝜑 ∨ 𝜒 ∨ 𝜏) ↔ (𝜓 ∨ 𝜃 ∨ 𝜂)))

Theorem

syl5imp 45086

Closed form of syl5 35. Derived automatically from syl5impVD 45436. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜃 → 𝜓) → (𝜑 → (𝜃 → 𝜒))))

Theorem

impexpd 45087

The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. After the User's Proof was completed, it was minimized. The completed User's Proof before minimization is not shown. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ (((𝜓 ∧ 𝜒) → 𝜃) ↔ (𝜓 → (𝜒 → 𝜃)))
qed:1:	⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃))))

⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃))))

Theorem

com3rgbi 45088

The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜑 → (𝜒 → (𝜓 → 𝜃))))
2::	⊢ ((𝜑 → (𝜒 → (𝜓 → 𝜃))) → (𝜒 → (𝜑 → (𝜓 → 𝜃))))
3:1,2:	⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) → (𝜒 → (𝜑 → (𝜓 → 𝜃))))
4::	⊢ ((𝜒 → (𝜑 → (𝜓 → 𝜃))) → (𝜑 → (𝜒 → (𝜓 → 𝜃))))
5::	⊢ ((𝜑 → (𝜒 → (𝜓 → 𝜃))) → (𝜑 → (𝜓 → (𝜒 → 𝜃))))
6:4,5:	⊢ ((𝜒 → (𝜑 → (𝜓 → 𝜃))) → (𝜑 → (𝜓 → (𝜒 → 𝜃))))
qed:3,6:	⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) ↔ (𝜒 → (𝜑 → (𝜓 → 𝜃))))

⊢ ((𝜑 → (𝜓 → (𝜒 → 𝜃))) ↔ (𝜒 → (𝜑 → (𝜓 → 𝜃))))

Theorem

impexpdcom 45089

The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃))))
2::	⊢ ((𝜓 → (𝜒 → (𝜑 → 𝜃))) ↔ (𝜑 → (𝜓 → (𝜒 → 𝜃))))
qed:1,2:	⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜓 → (𝜒 → (𝜑 → 𝜃))))

⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜓 → (𝜒 → (𝜑 → 𝜃))))

Theorem

ee1111 45090

Non-virtual deduction form of e1111 45249. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

h1::	⊢ (𝜑 → 𝜓)
h2::	⊢ (𝜑 → 𝜒)
h3::	⊢ (𝜑 → 𝜃)
h4::	⊢ (𝜑 → 𝜏)
h5::	⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))
6:1,5:	⊢ (𝜑 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))
7:6:	⊢ (𝜒 → (𝜑 → (𝜃 → (𝜏 → 𝜂))))
8:2,7:	⊢ (𝜑 → (𝜑 → (𝜃 → (𝜏 → 𝜂))))
9:8:	⊢ (𝜑 → (𝜃 → (𝜏 → 𝜂)))
10:9:	⊢ (𝜃 → (𝜑 → (𝜏 → 𝜂)))
11:3,10:	⊢ (𝜑 → (𝜑 → (𝜏 → 𝜂)))
12:11:	⊢ (𝜑 → (𝜏 → 𝜂))
13:12:	⊢ (𝜏 → (𝜑 → 𝜂))
14:4,13:	⊢ (𝜑 → (𝜑 → 𝜂))
qed:14:	⊢ (𝜑 → 𝜂)

⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ (𝜑 → 𝜃)    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜏 → 𝜂))))    ⇒   ⊢ (𝜑 → 𝜂)

Theorem

pm2.43bgbi 45091

Logical equivalence of a 2-left-nested implication and a 1-left-nested implicated when two antecedents of the former implication are identical. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

1::	⊢ ((𝜑 → (𝜓 → (𝜑 → 𝜒))) → (𝜑 → (𝜑 → (𝜓 → 𝜒))))
2::	⊢ ((𝜑 → (𝜑 → (𝜓 → 𝜒))) → (𝜑 → (𝜓 → 𝜒)))
3:1,2:	⊢ ((𝜑 → (𝜓 → (𝜑 → 𝜒))) → (𝜑 → (𝜓 → 𝜒)))
4::	⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))
5:3,4:	⊢ ((𝜑 → (𝜓 → (𝜑 → 𝜒))) → (𝜓 → (𝜑 → 𝜒)))
6::	⊢ ((𝜓 → (𝜑 → 𝜒)) → (𝜑 → (𝜓 → (𝜑 → 𝜒))))
qed:5,6:	⊢ ((𝜑 → (𝜓 → (𝜑 → 𝜒))) ↔ (𝜓 → (𝜑 → 𝜒)))

⊢ ((𝜑 → (𝜓 → (𝜑 → 𝜒))) ↔ (𝜓 → (𝜑 → 𝜒)))

Theorem

pm2.43cbi 45092

Logical equivalence of a 3-left-nested implication and a 2-left-nested implicated when two antecedents of the former implication are identical. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

1::	⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜑 → 𝜃))) ) → (𝜑 → (𝜓 → (𝜑 → (𝜒 → 𝜃)))))
2::	⊢ ((𝜑 → (𝜓 → (𝜑 → (𝜒 → 𝜃))) ) → (𝜓 → (𝜑 → (𝜒 → 𝜃))))
3:1,2:	⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜑 → 𝜃))) ) → (𝜓 → (𝜑 → (𝜒 → 𝜃))))
4::	⊢ ((𝜓 → (𝜑 → (𝜒 → 𝜃))) → (𝜓 → (𝜒 → (𝜑 → 𝜃))))
5:3,4:	⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜑 → 𝜃))) ) → (𝜓 → (𝜒 → (𝜑 → 𝜃))))
6::	⊢ ((𝜓 → (𝜒 → (𝜑 → 𝜃))) → (𝜑 → (𝜓 → (𝜒 → (𝜑 → 𝜃)))))
qed:5,6:	⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜑 → 𝜃))) ) ↔ (𝜓 → (𝜒 → (𝜑 → 𝜃))))

⊢ ((𝜑 → (𝜓 → (𝜒 → (𝜑 → 𝜃)))) ↔ (𝜓 → (𝜒 → (𝜑 → 𝜃))))

Theorem

ee233 45093

Non-virtual deduction form of e233 45338. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

h1::	⊢ (𝜑 → (𝜓 → 𝜒))
h2::	⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))
h3::	⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))
h4::	⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁)))
5:1,4:	⊢ (𝜑 → (𝜓 → (𝜏 → (𝜂 → 𝜁))) )
6:5:	⊢ (𝜏 → (𝜑 → (𝜓 → (𝜂 → 𝜁))) )
7:2,6:	⊢ (𝜑 → (𝜓 → (𝜃 → (𝜑 → (𝜓 → (𝜂 → 𝜁))))))
8:7:	⊢ (𝜓 → (𝜃 → (𝜑 → (𝜓 → (𝜂 → 𝜁)))))
9:8:	⊢ (𝜃 → (𝜑 → (𝜓 → (𝜂 → 𝜁))) )
10:9:	⊢ (𝜑 → (𝜓 → (𝜃 → (𝜂 → 𝜁))) )
11:10:	⊢ (𝜂 → (𝜑 → (𝜓 → (𝜃 → 𝜁))) )
12:3,11:	⊢ (𝜑 → (𝜓 → (𝜃 → (𝜑 → (𝜓 → (𝜃 → 𝜁))))))
13:12:	⊢ (𝜓 → (𝜃 → (𝜑 → (𝜓 → (𝜃 → 𝜁)))))
14:13:	⊢ (𝜃 → (𝜑 → (𝜓 → (𝜃 → 𝜁))) )
qed:14:	⊢ (𝜑 → (𝜓 → (𝜃 → 𝜁)))

⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏)))    &   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂)))    &   ⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜁)))

Theorem

imbi13 45094

Join three logical equivalences to form equivalence of implications. imbi13 45094 is imbi13VD 45447 without virtual deductions and was automatically derived from imbi13VD 45447 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ↔ 𝜃) → ((𝜏 ↔ 𝜂) → ((𝜑 → (𝜒 → 𝜏)) ↔ (𝜓 → (𝜃 → 𝜂))))))

Theorem

ee33 45095

Non-virtual deduction form of e33 45307. (Contributed by Alan Sare, 18-Mar-2012.) (Proof modification is discouraged.) (New usage is discouraged.) The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. The completed Virtual Deduction Proof (not shown) was minimized. The minimized proof is shown.

h1::	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
h2::	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))
h3::	⊢ (𝜃 → (𝜏 → 𝜂))
4:1,3:	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 → 𝜂))))
5:4:	⊢ (𝜏 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))
6:2,5:	⊢ (𝜑 → (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))))
7:6:	⊢ (𝜓 → (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂)))))
8:7:	⊢ (𝜒 → (𝜑 → (𝜓 → (𝜒 → 𝜂))))
qed:8:	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))    &   ⊢ (𝜃 → (𝜏 → 𝜂))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))

Theorem

con5 45096

Biconditional contraposition variation. This proof is con5VD 45473 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝜑 ↔ ¬ 𝜓) → (¬ 𝜑 → 𝜓))

Theorem

con5i 45097

Inference form of con5 45096. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 ↔ ¬ 𝜓)    ⇒   ⊢ (¬ 𝜑 → 𝜓)

Theorem

exlimexi 45098

Inference similar to Theorem 19.23 of [Margaris] p. 90. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (∃𝑥𝜑 → (𝜑 → 𝜓))    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)

Theorem

sb5ALT 45099*

Equivalence for substitution. Alternate proof of sb5 2313. This proof is sb5ALTVD 45486 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))

Theorem

eexinst01 45100

exinst01 45199 without virtual deductions. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ∃𝑥𝜓    &   ⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ (𝜑 → 𝜒)