P. 446 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

subrfv 44501

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

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

Theorem

mulvfv 44502

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

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

Theorem

addrfn 44503

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

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

Theorem

subrfn 44504

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

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

Theorem

mulvfn 44505

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

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

Theorem

addrcom 44506

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

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

Definition

df-ptdf 44507*

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 44508

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 44509*

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 8303 in 2008.

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

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 44510

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 44511

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

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

Theorem

3impexpbicom 44512

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

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

Theorem

3impexpbicomi 44513

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

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

21.41.2  Supplementary unification deductions

Theorem

bi1imp 44514

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 44515

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

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

Theorem

bi3impb 44516

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

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

Theorem

bi3impa 44517

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

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

Theorem

bi23impib 44518

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

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

Theorem

bi13impib 44519

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

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

Theorem

bi123impib 44520

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

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

Theorem

bi13impia 44521

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

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

Theorem

bi123impia 44522

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

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

Theorem

bi33imp12 44523

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

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

Theorem

bi13imp23 44524

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

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

Theorem

bi13imp2 44525

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

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

Theorem

bi12imp3 44526

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

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

Theorem

bi23imp1 44527

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

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

Theorem

bi123imp0 44528

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

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

Theorem

4animp1 44529

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 44530

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

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

Theorem

4an4132 44531

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

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

Theorem

expcomdg 44532

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 44533

idn3 44647 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 44534

e222 44668 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 44535

Right-biconditional form of e3 44768 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 44536

e13 44779 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 44537

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

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

Theorem

ee122 44538

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

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

Theorem

ee333 44539

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

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

Theorem

ee323 44540

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

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

Theorem

3ornot23 44541

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

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

Theorem

orbi1r 44542

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

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

Theorem

3orbi123 44543

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

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

Theorem

syl5imp 44544

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

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

Theorem

impexpd 44545

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 44546

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 44547

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 44548

Non-virtual deduction form of e1111 44707. (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 44549

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 44550

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 44551

Non-virtual deduction form of e233 44796. (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 44552

Join three logical equivalences to form equivalence of implications. imbi13 44552 is imbi13VD 44905 without virtual deductions and was automatically derived from imbi13VD 44905 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 44553

Non-virtual deduction form of e33 44765. (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 44554

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

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

Theorem

con5i 44555

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

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

Theorem

exlimexi 44556

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 44557*

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

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

Theorem

eexinst01 44558

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

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

Theorem

eexinst11 44559

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

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

Theorem

vk15.4j 44560

Excercise 4j of Unit 15 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. This proof is the minimized Hilbert-style axiomatic version of the Fitch-style Natural Deduction proof found on page 442 of Klenk and was automatically derived from that proof. vk15.4j 44560 is vk15.4jVD 44945 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))    &   ⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏))    &   ⊢ ¬ ∀𝑥(𝜏 → 𝜑)    ⇒   ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Theorem

notnotrALT 44561

Converse of double negation. Alternate proof of notnotr 130. This proof is notnotrALTVD 44946 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (¬ ¬ 𝜑 → 𝜑)

Theorem

con3ALT2 44562

Contraposition. Alternate proof of con3 153. This proof is con3ALTVD 44947 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

ssralv2 44563*

Quantification restricted to a subclass for two quantifiers. ssralv 4003 for two quantifiers. The proof of ssralv2 44563 was automatically generated by minimizing the automatically translated proof of ssralv2VD 44897. The automatic translation is by the tools program translate_without_overwriting.cmd. (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝜑))

Theorem

sbc3or 44564

sbcor 3792 with a 3-disjuncts. This proof is sbc3orgVD 44882 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Revised by NM, 24-Aug-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ([𝐴 / 𝑥]𝜑 ∨ [𝐴 / 𝑥]𝜓 ∨ [𝐴 / 𝑥]𝜒))

Theorem

alrim3con13v 44565*

Closed form of alrimi 2216 with 2 additional conjuncts having no occurrences of the quantifying variable. This proof is 19.21a3con13vVD 44883 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝜑 → ∀𝑥𝜑) → ((𝜓 ∧ 𝜑 ∧ 𝜒) → ∀𝑥(𝜓 ∧ 𝜑 ∧ 𝜒)))

Theorem

rspsbc2 44566*

rspsbc 3830 with two quantifying variables. This proof is rspsbc2VD 44886 automatically translated and minimized. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ 𝐵 → (𝐶 ∈ 𝐷 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐷 𝜑 → [𝐶 / 𝑦][𝐴 / 𝑥]𝜑)))

Theorem

sbcoreleleq 44567*

Substitution of a setvar variable for another setvar variable in a 3-conjunct formula. Derived automatically from sbcoreleleqVD 44890. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑦](𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴)))

Theorem

tratrb 44568*

If a class is transitive and any two distinct elements of the class are E-comparable, then every element of that class is transitive. Derived automatically from tratrbVD 44892. (Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐵)

Theorem

ordelordALT 44569

An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 6328 using the Axiom of Regularity indirectly through dford2 9510. dford2 is a weaker definition of ordinal number. Given the Axiom of Regularity, it need not be assumed that E Fr 𝐴 because this is inferred by the Axiom of Regularity. ordelordALT 44569 is ordelordALTVD 44898 without virtual deductions and was automatically derived from ordelordALTVD 44898 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

sbcim2g 44570

Distribution of class substitution over a left-nested implication. Similar to sbcimg 3790. sbcim2g 44570 is sbcim2gVD 44906 without virtual deductions and was automatically derived from sbcim2gVD 44906 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

sbcbi 44571

Implication form of sbcbii 3798. sbcbi 44571 is sbcbiVD 44907 without virtual deductions and was automatically derived from sbcbiVD 44907 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

trsbc 44572*

Formula-building inference rule for class substitution, substituting a class variable for the setvar variable of the transitivity predicate. trsbc 44572 is trsbcVD 44908 without virtual deductions and was automatically derived from trsbcVD 44908 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.)

⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]Tr 𝑥 ↔ Tr 𝐴))

Theorem

truniALT 44573*

The union of a class of transitive sets is transitive. Alternate proof of truni 5213. truniALT 44573 is truniALTVD 44909 without virtual deductions and was automatically derived from truniALTVD 44909 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.)

⊢ (∀𝑥 ∈ 𝐴 Tr 𝑥 → Tr ∪ 𝐴)

Theorem

onfrALTlem5 44574*

Lemma for onfrALT 44581. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ([(𝑎 ∩ 𝑥) / 𝑏]((𝑏 ⊆ (𝑎 ∩ 𝑥) ∧ 𝑏 ≠ ∅) → ∃𝑦 ∈ 𝑏 (𝑏 ∩ 𝑦) = ∅) ↔ (((𝑎 ∩ 𝑥) ⊆ (𝑎 ∩ 𝑥) ∧ (𝑎 ∩ 𝑥) ≠ ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))

Theorem

onfrALTlem4 44575*

Lemma for onfrALT 44581. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅))

Theorem

onfrALTlem3 44576*

Lemma for onfrALT 44581. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ∃𝑦 ∈ (𝑎 ∩ 𝑥)((𝑎 ∩ 𝑥) ∩ 𝑦) = ∅))

Theorem

ggen31 44577*

gen31 44653 without virtual deductions. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))    ⇒   ⊢ (𝜑 → (𝜓 → (𝜒 → ∀𝑥𝜃)))

Theorem

onfrALTlem2 44578*

Lemma for onfrALT 44581. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ ¬ (𝑎 ∩ 𝑥) = ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅))

Theorem

cbvexsv 44579*

A theorem pertaining to the substitution for an existentially quantified variable when the substituted variable does not occur in the quantified wff. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

onfrALTlem1 44580*

Lemma for onfrALT 44581. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝑎 ⊆ On ∧ 𝑎 ≠ ∅) → ((𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) → ∃𝑦 ∈ 𝑎 (𝑎 ∩ 𝑦) = ∅))

Theorem

onfrALT 44581

The membership relation is foundational on the class of ordinal numbers. onfrALT 44581 is an alternate proof of onfr 6345. onfrALTVD 44922 is the Virtual Deduction proof from which onfrALT 44581 is derived. The Virtual Deduction proof mirrors the working proof of onfr 6345 which is the main part of the proof of Theorem 7.12 of the first edition of TakeutiZaring. The proof of the corresponding Proposition 7.12 of [TakeutiZaring] p. 38 (second edition) does not contain the working proof equivalent of onfrALTVD 44922. This theorem does not rely on the Axiom of Regularity. (Contributed by Alan Sare, 22-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ E Fr On

Theorem

19.41rg 44582

Closed form of right-to-left implication of 19.41 2238, Theorem 19.41 of [Margaris] p. 90. Derived from 19.41rgVD 44933. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (∀𝑥(𝜓 → ∀𝑥𝜓) → ((∃𝑥𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ 𝜓)))

Theorem

opelopab4 44583*

Ordered pair membership in a class abstraction of ordered pairs. Compare to elopab 5467. (Contributed by Alan Sare, 8-Feb-2014.) (Revised by Mario Carneiro, 6-May-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (⟨𝑢, 𝑣⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))

Theorem

2pm13.193 44584

pm13.193 44443 for two variables. pm13.193 44443 is Theorem *13.193 in [WhiteheadRussell] p. 179. Derived from 2pm13.193VD 44934. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

hbntal 44585

A closed form of hbn 2297. hbnt 2296 is another closed form of hbn 2297. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → ∀𝑥(¬ 𝜑 → ∀𝑥 ¬ 𝜑))

Theorem

hbimpg 44586

A closed form of hbim 2301. Derived from hbimpgVD 44935. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((∀𝑥(𝜑 → ∀𝑥𝜑) ∧ ∀𝑥(𝜓 → ∀𝑥𝜓)) → ∀𝑥((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)))

Theorem

hbalg 44587

Closed form of hbal 2170. Derived from hbalgVD 44936. (Contributed by Alan Sare, 8-Feb-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑦(∀𝑦𝜑 → ∀𝑥∀𝑦𝜑))

Theorem

hbexg 44588

Closed form of nfex 2325. Derived from hbexgVD 44937. (Contributed by Alan Sare, 8-Feb-2014.) (Revised by Mario Carneiro, 12-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (∀𝑥∀𝑦(𝜑 → ∀𝑥𝜑) → ∀𝑥∀𝑦(∃𝑦𝜑 → ∀𝑥∃𝑦𝜑))

Theorem

ax6e2eq 44589*

Alternate form of ax6e 2383 for non-distinct 𝑥, 𝑦 and 𝑢 = 𝑣. ax6e2eq 44589 is derived from ax6e2eqVD 44938. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (∀𝑥 𝑥 = 𝑦 → (𝑢 = 𝑣 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣)))

Theorem

ax6e2nd 44590*

If at least two sets exist (dtru 5379), then the same is true expressed in an alternate form similar to the form of ax6e 2383. ax6e2nd 44590 is derived from ax6e2ndVD 44939. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Theorem

ax6e2ndeq 44591*

"At least two sets exist" expressed in the form of dtru 5379 is logically equivalent to the same expressed in a form similar to ax6e 2383 if dtru 5379 is false implies 𝑢 = 𝑣. ax6e2ndeq 44591 is derived from ax6e2ndeqVD 44940. (Contributed by Alan Sare, 25-Mar-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Theorem

2sb5nd 44592*

Equivalence for double substitution 2sb5 2280 without distinct 𝑥, 𝑦 requirement. 2sb5nd 44592 is derived from 2sb5ndVD 44941. (Contributed by Alan Sare, 30-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))

Theorem

2uasbanh 44593*

Distribute the unabbreviated form of proper substitution in and out of a conjunction. 2uasbanh 44593 is derived from 2uasbanhVD 44942. (Contributed by Alan Sare, 31-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜒 ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))    ⇒   ⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))

Theorem

2uasban 44594*

Distribute the unabbreviated form of proper substitution in and out of a conjunction. (Contributed by Alan Sare, 31-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))

Theorem

e2ebind 44595

Absorption of an existential quantifier of a double existential quantifier of non-distinct variables. e2ebind 44595 is derived from e2ebindVD 44943. (Contributed by Alan Sare, 27-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

elpwgded 44596

elpwgdedVD 44948 in conventional notation. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → 𝐴 ∈ V)    &   ⊢ (𝜓 → 𝐴 ⊆ 𝐵)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ 𝒫 𝐵)

Theorem

trelded 44597

Deduction form of trel 5206. In a transitive class, the membership relation is transitive. (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → Tr 𝐴)    &   ⊢ (𝜓 → 𝐵 ∈ 𝐶)    &   ⊢ (𝜒 → 𝐶 ∈ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝐵 ∈ 𝐴)

Theorem

jaoded 44598

Deduction form of jao 962. Disjunction of antecedents. (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Theorem

sbtT 44599

A substitution into a theorem remains true. sbt 2069 with the existence of no virtual hypotheses for the hypothesis expressed as the empty virtual hypothesis collection. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (⊤ → 𝜑)    ⇒   ⊢ [𝑦 / 𝑥]𝜑

Theorem

not12an2impnot1 44600

If a double conjunction is false and the second conjunct is true, then the first conjunct is false. https://us.metamath.org/other/completeusersproof/not12an2impnot1vd.html is the Virtual Deduction proof verified by automatically transforming it into the Metamath proof of not12an2impnot1 44600 using completeusersproof, which is verified by the Metamath program. https://us.metamath.org/other/completeusersproof/not12an2impnot1ro.html 44600 is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018.)

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