P. 445 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 44401-44500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pm13.194 44401	Theorem *13.194 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) ↔ ([𝑦 / 𝑥]𝜑 ∧ 𝜑 ∧ 𝑥 = 𝑦))
Theorem	pm13.195 44402*	Theorem *13.195 in [WhiteheadRussell] p. 179. This theorem is very similar to sbc5 3781. (Contributed by Andrew Salmon, 3-Jun-2011.) (Revised by NM, 4-Jan-2017.)
⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ [𝐴 / 𝑦]𝜑)
Theorem	pm13.196a 44403*	Theorem *13.196 in [WhiteheadRussell] p. 179. The only difference is the position of the substituted variable. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ (¬ 𝜑 ↔ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))
Theorem	2sbc6g 44404*	Theorem *13.21 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑧∀𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) → 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))
Theorem	2sbc5g 44405*	Theorem *13.22 in [WhiteheadRussell] p. 179. (Contributed by Andrew Salmon, 3-Jun-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∃𝑧∃𝑤((𝑧 = 𝐴 ∧ 𝑤 = 𝐵) ∧ 𝜑) ↔ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑))
Theorem	iotain 44406	Equivalence between two different forms of ℩. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∩ {𝑥 ∣ 𝜑} = (℩𝑥𝜑))
Theorem	iotaexeu 44407	The iota class exists. This theorem does not require ax-nul 5261 for its proof. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → (℩𝑥𝜑) ∈ V)
Theorem	iotasbc 44408*	Definition *14.01 in [WhiteheadRussell] p. 184. In Principia Mathematica, Russell and Whitehead define ℩ in terms of a function of (℩𝑥𝜑). Their definition differs in that a function of (℩𝑥𝜑) evaluates to "false" when there isn't a single 𝑥 that satisfies 𝜑. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑦]𝜓 ↔ ∃𝑦(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ 𝜓)))
Theorem	iotasbc2 44409*	Theorem *14.111 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ ((∃!𝑥𝜑 ∧ ∃!𝑥𝜓) → ([(℩𝑥𝜑) / 𝑦][(℩𝑥𝜓) / 𝑧]𝜒 ↔ ∃𝑦∃𝑧(∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∀𝑥(𝜓 ↔ 𝑥 = 𝑧) ∧ 𝜒)))
Theorem	pm14.12 44410*	Theorem *14.12 in [WhiteheadRussell] p. 184. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
Theorem	pm14.122a 44411*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑)))
Theorem	pm14.122b 44412*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → ((∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ [𝐴 / 𝑥]𝜑) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑)))
Theorem	pm14.122c 44413*	Theorem *14.122 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝜑 ↔ 𝑥 = 𝐴) ↔ (∀𝑥(𝜑 → 𝑥 = 𝐴) ∧ ∃𝑥𝜑)))
Theorem	pm14.123a 44414*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑)))
Theorem	pm14.123b 44415*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ [𝐴 / 𝑧][𝐵 / 𝑤]𝜑) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑)))
Theorem	pm14.123c 44416*	Theorem *14.123 in [WhiteheadRussell] p. 185. (Contributed by Andrew Salmon, 9-Jun-2011.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (∀𝑧∀𝑤(𝜑 ↔ (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ↔ (∀𝑧∀𝑤(𝜑 → (𝑧 = 𝐴 ∧ 𝑤 = 𝐵)) ∧ ∃𝑧∃𝑤𝜑)))
Theorem	pm14.18 44417	Theorem *14.18 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∀𝑥𝜓 → [(℩𝑥𝜑) / 𝑥]𝜓))
Theorem	iotaequ 44418*	Theorem *14.2 in [WhiteheadRussell] p. 189. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (℩𝑥𝑥 = 𝑦) = 𝑦
Theorem	iotavalb 44419*	Theorem *14.202 in [WhiteheadRussell] p. 189. A biconditional version of iotaval 6482. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (℩𝑥𝜑) = 𝑦))
Theorem	iotasbc5 44420*	Theorem *14.205 in [WhiteheadRussell] p. 190. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!𝑥𝜑 → ([(℩𝑥𝜑) / 𝑦]𝜓 ↔ ∃𝑦(𝑦 = (℩𝑥𝜑) ∧ 𝜓)))
Theorem	pm14.24 44421*	Theorem *14.24 in [WhiteheadRussell] p. 191. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝑦 = (℩𝑥𝜑)))
Theorem	iotavalsb 44422*	Theorem *14.242 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ([𝑦 / 𝑧]𝜓 ↔ [(℩𝑥𝜑) / 𝑧]𝜓))
Theorem	sbiota1 44423	Theorem *14.25 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓))
Theorem	sbaniota 44424	Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 12-Jul-2011.)
⊢ (∃!𝑥𝜑 → (∃𝑥(𝜑 ∧ 𝜓) ↔ [(℩𝑥𝜑) / 𝑥]𝜓))
Theorem	eubiOLD 44425	Obsolete proof of eubi 2577 as of 7-Oct-2022. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
Theorem	iotasbcq 44426	Theorem *14.272 in [WhiteheadRussell] p. 193. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([(℩𝑥𝜑) / 𝑦]𝜒 ↔ [(℩𝑥𝜓) / 𝑦]𝜒))
21.40.5  Set Theory
Theorem	elnev 44427*	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 44428	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 44429*	Equality between two ways of saying "the complement of 𝐴". (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (V ∖ 𝐴) = {𝑥 ∣ ¬ 𝑥 ∈ 𝐴}
Theorem	compne 44430	The complement of 𝐴 is not equal to 𝐴. (Contributed by Andrew Salmon, 15-Jul-2011.) (Proof shortened by BJ, 11-Nov-2021.)
⊢ (V ∖ 𝐴) ≠ 𝐴
Theorem	compab 44431	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 44432	Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ (𝐴 ⊆ (V ∖ 𝐵) ↔ 𝐵 ⊆ (V ∖ 𝐴))
Theorem	conss1 44433	Contrapositive law for subsets. (Contributed by Andrew Salmon, 15-Jul-2011.)
⊢ ((V ∖ 𝐴) ⊆ 𝐵 ↔ (V ∖ 𝐵) ⊆ 𝐴)
Theorem	ralbidar 44434	More general form of ralbida 3248. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝐴 𝜒))
Theorem	rexbidar 44435	More general form of rexbida 3249. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜑)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 𝜒))
Theorem	dropab1 44436	Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (∀𝑥 𝑥 = 𝑦 → {⟨𝑥, 𝑧⟩ ∣ 𝜑} = {⟨𝑦, 𝑧⟩ ∣ 𝜑})
Theorem	dropab2 44437	Theorem to aid use of the distinctor reduction theorem with ordered pair class abstraction. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (∀𝑥 𝑥 = 𝑦 → {⟨𝑧, 𝑥⟩ ∣ 𝜑} = {⟨𝑧, 𝑦⟩ ∣ 𝜑})
Theorem	ipo0 44438	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 44439	A class that is founded by the identity relation is null. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ ( I Fr 𝐴 ↔ 𝐴 = ∅)
Theorem	ordpss 44440	ordelpss 6360 with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011.)
⊢ (Ord 𝐵 → (𝐴 ∈ 𝐵 → 𝐴 ⊊ 𝐵))
Theorem	fvsb 44441*	Explicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (∃!𝑦 𝐴𝐹𝑦 → ([(𝐹‘𝐴) / 𝑥]𝜑 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑)))
Theorem	fveqsb 44442*	Implicit substitution of a value of a function into a wff. (Contributed by Andrew Salmon, 1-Aug-2011.)
⊢ (𝑥 = (𝐹‘𝐴) → (𝜑 ↔ 𝜓))    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃!𝑦 𝐴𝐹𝑦 → (𝜓 ↔ ∃𝑥(∀𝑦(𝐴𝐹𝑦 ↔ 𝑦 = 𝑥) ∧ 𝜑)))
Theorem	xpexb 44443	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 44444	An element of a transitive set is a proper subset of it. Theorem 7.2 in [TakeutiZaring] p. 35. Unlike tz7.2 5621, ax-reg 9545 is required for its proof. (Contributed by Andrew Salmon, 13-Nov-2011.)
⊢ ((Tr 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊊ 𝐴)
21.40.6  Arithmetic
Theorem	addcomgi 44445	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 44446	Introduce the operation of vector addition.
class +𝑟
Syntax	cminusr 44447	Introduce the operation of vector subtraction.
class -𝑟
Syntax	ctimesr 44448	Introduce the operation of scalar multiplication.
class .𝑣
Syntax	cptdfc 44449	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 44450	RR3 is a class.
class RR3
Syntax	cline3 44451	line3 is a class.
class line3
Definition	df-addr 44452*	Define the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ +𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) + (𝑦‘𝑣))))
Definition	df-subr 44453*	Define the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ -𝑟 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ ((𝑥‘𝑣) − (𝑦‘𝑣))))
Definition	df-mulv 44454*	Define the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ .𝑣 = (𝑥 ∈ V, 𝑦 ∈ V ↦ (𝑣 ∈ ℝ ↦ (𝑥 · (𝑦‘𝑣))))
Theorem	addrval 44455*	Value of the operation of vector addition. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) + (𝐵‘𝑣))))
Theorem	subrval 44456*	Value of the operation of vector subtraction. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-𝑟𝐵) = (𝑣 ∈ ℝ ↦ ((𝐴‘𝑣) − (𝐵‘𝑣))))
Theorem	mulvval 44457*	Value of the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴.𝑣𝐵) = (𝑣 ∈ ℝ ↦ (𝐴 · (𝐵‘𝑣))))
Theorem	addrfv 44458	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 44459	Vector subtraction at a value. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴-𝑟𝐵)‘𝐶) = ((𝐴‘𝐶) − (𝐵‘𝐶)))
Theorem	mulvfv 44460	Scalar multiplication at a value. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐸 ∧ 𝐵 ∈ 𝐷 ∧ 𝐶 ∈ ℝ) → ((𝐴.𝑣𝐵)‘𝐶) = (𝐴 · (𝐵‘𝐶)))
Theorem	addrfn 44461	Vector addition produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) Fn ℝ)
Theorem	subrfn 44462	Vector subtraction produces a function. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴-𝑟𝐵) Fn ℝ)
Theorem	mulvfn 44463	Scalar multiplication producees a function. (Contributed by Andrew Salmon, 27-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴.𝑣𝐵) Fn ℝ)
Theorem	addrcom 44464	Vector addition is commutative. (Contributed by Andrew Salmon, 28-Jan-2012.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴+𝑟𝐵) = (𝐵+𝑟𝐴))
Definition	df-ptdf 44465*	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 44466	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 44467*	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 ∣ (2o ≼ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑧 ≠ 𝑦 → 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 8352 in 2008. He developed a tool called "completeusersproof" that assists developing proofs using his "virtual deduction" method: https://us.metamath.org/other.html#completeusersproof 8352. His virtual deduction method is explained in the comment for wvd1 44559. 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 44468	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 44469	Exportation implication also converting the consequent from a biconditional to an implication. Derived automatically from exbirVD 44842. (Contributed by Alan Sare, 31-Dec-2011.)
⊢ (((𝜑 ∧ 𝜓) → (𝜒 ↔ 𝜃)) → (𝜑 → (𝜓 → (𝜃 → 𝜒))))
Theorem	3impexpbicom 44470	Version of 3impexp 1359 where in addition the consequent is commuted. (Contributed by Alan Sare, 31-Dec-2011.)
⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏)) ↔ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃)))))
Theorem	3impexpbicomi 44471	Inference associated with 3impexpbicom 44470. Derived automatically from 3impexpbicomiVD 44847. (Contributed by Alan Sare, 31-Dec-2011.)
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 ↔ 𝜏))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜏 ↔ 𝜃))))
21.41.2  Supplementary unification deductions
Theorem	bi1imp 44472	Importation inference similar to imp 406, except the outermost implication of the hypothesis is a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (𝜑 ↔ (𝜓 → 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	bi2imp 44473	Importation inference similar to imp 406, except both implications of the hypothesis are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (𝜑 ↔ (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
Theorem	bi3impb 44474	Similar to 3impb 1114 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi3impa 44475	Similar to 3impa 1109 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ 𝜃)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi23impib 44476	3impib 1116 with the inner implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi13impib 44477	3impib 1116 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (𝜑 ↔ ((𝜓 ∧ 𝜒) → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi123impib 44478	3impib 1116 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (𝜑 ↔ ((𝜓 ∧ 𝜒) ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi13impia 44479	3impia 1117 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜒 → 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi123impia 44480	3impia 1117 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ ((𝜑 ∧ 𝜓) ↔ (𝜒 ↔ 𝜃))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi33imp12 44481	3imp 1110 with innermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi13imp23 44482	3imp 1110 with outermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (𝜑 ↔ (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi13imp2 44483	Similar to 3imp 1110 except the outermost and innermost implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (𝜑 ↔ (𝜓 → (𝜒 ↔ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi12imp3 44484	Similar to 3imp 1110 except all but innermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (𝜑 ↔ (𝜓 ↔ (𝜒 → 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi23imp1 44485	Similar to 3imp 1110 except all but outermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (𝜑 → (𝜓 ↔ (𝜒 ↔ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	bi123imp0 44486	Similar to 3imp 1110 except all implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.)
⊢ (𝜑 ↔ (𝜓 ↔ (𝜒 ↔ 𝜃)))    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
Theorem	4animp1 44487	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 44488	A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.)
⊢ ((((𝜒 ∧ 𝜓) ∧ 𝜑) ∧ 𝜃) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	4an4132 44489	A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.)
⊢ ((((𝜃 ∧ 𝜒) ∧ 𝜓) ∧ 𝜑) → 𝜏)    ⇒   ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜏)
Theorem	expcomdg 44490	Biconditional form of expcomd 416. (Contributed by Alan Sare, 22-Jul-2012.) (New usage is discouraged.)
⊢ ((𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) ↔ (𝜑 → (𝜒 → (𝜓 → 𝜃))))
21.41.3  Conventional Metamath proofs, some derived from VD proofs
Theorem	iidn3 44491	idn3 44605 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 44492	e222 44626 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 44493	Right-biconditional form of e3 44726 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 44494	e13 44737 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 44495	e121 44646 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜂))
Theorem	ee122 44496	e122 44643 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ (𝜑 → (𝜒 → 𝜃))    &   ⊢ (𝜑 → (𝜒 → 𝜏))    &   ⊢ (𝜓 → (𝜃 → (𝜏 → 𝜂)))    ⇒   ⊢ (𝜑 → (𝜒 → 𝜂))
Theorem	ee333 44497	e333 44722 without virtual deductions. (Contributed by Alan Sare, 17-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜏)))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))    &   ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜁)))
Theorem	ee323 44498	e323 44755 without virtual deductions. (Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    &   ⊢ (𝜑 → (𝜓 → 𝜏))    &   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂)))    &   ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜁)))
Theorem	3ornot23 44499	If the second and third disjuncts of a true triple disjunction are false, then the first disjunct is true. Automatically derived from 3ornot23VD 44836. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒))
Theorem	orbi1r 44500	orbi1 917 with order of disjuncts reversed. Derived from orbi1rVD 44837. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓)))