Theorem List for Metamath Proof Explorer - 39901-40000 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ee13an 39901 |
e13an 39900 without virtual deductions. (Contributed by
Alan Sare,
8-Jul-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜏))) & ⊢ ((𝜓 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜒 → (𝜃 → 𝜂))) |
|
Theorem | e31 39902 |
A virtual deduction elimination rule. (Contributed by Alan Sare,
13-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) |
|
Theorem | ee31 39903 |
e31 39902 without virtual deductions. (Contributed by
Alan Sare,
25-Jul-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → 𝜏)
& ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) |
|
Theorem | e31an 39904 |
A virtual deduction elimination rule. (Contributed by Alan Sare,
24-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 ▶ 𝜏 ) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) |
|
Theorem | ee31an 39905 |
e31an 39904 without virtual deductions. (Contributed by
Alan Sare,
14-Jul-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → 𝜏)
& ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) |
|
Theorem | e23 39906 |
A virtual deduction elimination rule (see syl10 79). (Contributed by
Alan Sare, 12-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ (𝜒 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜂 ) |
|
Theorem | e23an 39907 |
A virtual deduction elimination rule. (Contributed by Alan Sare,
24-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜂 ) |
|
Theorem | ee23an 39908 |
e23an 39907 without virtual deductions. (Contributed by
Alan Sare,
14-Jul-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜏))) & ⊢ ((𝜒 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜂))) |
|
Theorem | e32 39909 |
A virtual deduction elimination rule. (Contributed by Alan Sare,
12-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) |
|
Theorem | ee32 39910 |
e32 39909 without virtual deductions. (Contributed by
Alan Sare,
18-Jul-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ (𝜃 → (𝜏 → 𝜂)) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) |
|
Theorem | e32an 39911 |
A virtual deduction elimination rule. (Contributed by Alan Sare,
24-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) |
|
Theorem | ee32an 39912 |
e33an 39886 without virtual deductions. (Contributed by
Alan Sare,
14-Jul-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) & ⊢ (𝜑 → (𝜓 → 𝜏)) & ⊢ ((𝜃 ∧ 𝜏) → 𝜂) ⇒ ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜂))) |
|
Theorem | e123 39913 |
A virtual deduction elimination rule. (Contributed by Alan Sare,
12-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜑 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜒 , 𝜏 ▶ 𝜂 ) & ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜒 , 𝜏 ▶ 𝜁 ) |
|
Theorem | ee123 39914 |
e123 39913 without virtual deductions. (Contributed by
Alan Sare,
25-Jul-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝜑 → 𝜓)
& ⊢ (𝜑 → (𝜒 → 𝜃)) & ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜂))) & ⊢ (𝜓 → (𝜃 → (𝜂 → 𝜁))) ⇒ ⊢ (𝜑 → (𝜒 → (𝜏 → 𝜁))) |
|
Theorem | el123 39915 |
A virtual deduction elimination rule. (Contributed by Alan Sare,
13-Jun-2015.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ( 𝜑 ▶ 𝜓 ) & ⊢ ( 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜏 ▶ 𝜂 ) & ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁) ⇒ ⊢ ( ( 𝜑 , 𝜒 , 𝜏 ) ▶ 𝜁 ) |
|
Theorem | e233 39916 |
A virtual deduction elimination rule. (Contributed by Alan Sare,
29-Feb-2012.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ( 𝜑 , 𝜓 ▶ 𝜒 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜏 ) & ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜂 ) & ⊢ (𝜒 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜃 ▶ 𝜁 ) |
|
Theorem | e323 39917 |
A virtual deduction elimination rule. (Contributed by Alan Sare,
17-Apr-2012.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜃 ) & ⊢ ( 𝜑 , 𝜓 ▶ 𝜏 ) & ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜂 ) & ⊢ (𝜃 → (𝜏 → (𝜂 → 𝜁))) ⇒ ⊢ ( 𝜑 , 𝜓 , 𝜒 ▶ 𝜁 ) |
|
Theorem | e000 39918 |
A virtual deduction elimination rule. The non-virtual deduction form of
e000 39918 is the virtual deduction form. (Contributed
by Alan Sare,
14-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 𝜑 & ⊢ 𝜓 & ⊢ 𝜒 & ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) ⇒ ⊢ 𝜃 |
|
Theorem | e00 39919 |
Elimination rule identical to mp2 9. The non-virtual deduction form is
the virtual deduction form, which is mp2 9.
(Contributed by Alan Sare,
14-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 𝜑 & ⊢ 𝜓 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ 𝜒 |
|
Theorem | e00an 39920 |
Elimination rule identical to mp2an 682. The non-virtual deduction form
is the virtual deduction form, which is mp2an 682. (Contributed by Alan
Sare, 15-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 |
|
Theorem | eel00cT 39921 |
An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ 𝜑 & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (⊤ → 𝜒) |
|
Theorem | eelTT 39922 |
An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (⊤
→ 𝜑) & ⊢ (⊤
→ 𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 |
|
Theorem | e0a 39923 |
Elimination rule identical to ax-mp 5. The non-virtual deduction form
is the virtual deduction form, which is ax-mp 5.
(Contributed by Alan
Sare, 14-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ 𝜓 |
|
Theorem | eelT 39924 |
An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (⊤
→ 𝜑) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ 𝜓 |
|
Theorem | eel0cT 39925 |
An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ 𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (⊤ → 𝜓) |
|
Theorem | eelT0 39926 |
An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (⊤
→ 𝜑) & ⊢ 𝜓 & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ 𝜒 |
|
Theorem | e0bi 39927 |
Elimination rule identical to mpbi 222. The non-virtual deduction form
is the virtual deduction form, which is mpbi 222.
(Contributed by Alan
Sare, 15-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 𝜑 & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ 𝜓 |
|
Theorem | e0bir 39928 |
Elimination rule identical to mpbir 223. The non-virtual deduction form
is the virtual deduction form, which is mpbir 223. (Contributed by Alan
Sare, 15-Jun-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 𝜑 & ⊢ (𝜓 ↔ 𝜑) ⇒ ⊢ 𝜓 |
|
Theorem | uun0.1 39929 |
Convention notation form of un0.1 39930. (Contributed by Alan Sare,
23-Apr-2015.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (⊤
→ 𝜑) & ⊢ (𝜓 → 𝜒)
& ⊢ ((⊤ ∧ 𝜓) → 𝜃) ⇒ ⊢ (𝜓 → 𝜃) |
|
Theorem | un0.1 39930 |
⊤ is the constant true, a tautology (see df-tru 1605). Kleene's
"empty conjunction" is logically equivalent to ⊤. In a virtual
deduction we shall interpret ⊤ to be the
empty wff or the empty
collection of virtual hypotheses. ⊤ in a
virtual deduction
translated into conventional notation we shall interpret to be Kleene's
empty conjunction. If 𝜃 is true given the empty collection
of
virtual hypotheses and another collection of virtual hypotheses, then it
is true given only the other collection of virtual hypotheses.
(Contributed by Alan Sare, 23-Apr-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ( ⊤ ▶ 𝜑 ) & ⊢ ( 𝜓 ▶ 𝜒 ) & ⊢ ( ( ⊤ , 𝜓 ) ▶ 𝜃 )
⇒ ⊢ ( 𝜓 ▶ 𝜃 ) |
|
Theorem | uunT1 39931 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 3-Dec-2015.) Proof was revised to
accommodate a possible future version of df-tru 1605. (Revised by David
A. Wheeler, 8-May-2019.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ((⊤
∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | uunT1p1 39932 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ∧ ⊤) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | uunT21 39933 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 3-Dec-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((⊤
∧ (𝜑 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | uun121 39934 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ∧ (𝜑 ∧ 𝜓)) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | uun121p1 39935 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | uun132 39936 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | uun132p1 39937 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (((𝜓 ∧ 𝜒) ∧ 𝜑) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | anabss7p1 39938 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
This would have been named uun221 if the 0th permutation did not exist
in set.mm as anabss7 663. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (((𝜓 ∧ 𝜑) ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
|
Theorem | un10 39939 |
A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ( ( 𝜑 , ⊤ ) ▶ 𝜓 )
⇒ ⊢ ( 𝜑 ▶ 𝜓 ) |
|
Theorem | un01 39940 |
A unionizing deduction. (Contributed by Alan Sare, 28-Apr-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ( ( ⊤ , 𝜑 ) ▶ 𝜓 )
⇒ ⊢ ( 𝜑 ▶ 𝜓 ) |
|
Theorem | un2122 39941 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 3-Dec-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ 𝜓 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | uun2131 39942 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (((𝜑 ∧ 𝜓) ∧ (𝜑 ∧ 𝜒)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | uun2131p1 39943 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (((𝜑 ∧ 𝜒) ∧ (𝜑 ∧ 𝜓)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | uunTT1 39944 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((⊤
∧ ⊤ ∧ 𝜑)
→ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | uunTT1p1 39945 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((⊤
∧ 𝜑 ∧ ⊤)
→ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | uunTT1p2 39946 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ∧ ⊤ ∧ ⊤)
→ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | uunT11 39947 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((⊤
∧ 𝜑 ∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | uunT11p1 39948 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ∧ ⊤ ∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | uunT11p2 39949 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ∧ 𝜑 ∧ ⊤) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | uunT12 39950 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((⊤
∧ 𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | uunT12p1 39951 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((⊤
∧ 𝜓 ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | uunT12p2 39952 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ∧ ⊤ ∧ 𝜓) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | uunT12p3 39953 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜓 ∧ ⊤ ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | uunT12p4 39954 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ ⊤) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | uunT12p5 39955 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜓 ∧ 𝜑 ∧ ⊤) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | uun111 39956 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ∧ 𝜑 ∧ 𝜑) → 𝜓) ⇒ ⊢ (𝜑 → 𝜓) |
|
Theorem | 3anidm12p1 39957 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
3anidm12 1491 denotes the deduction which would have been
named uun112 if
it did not pre-exist in set.mm. This second permutation's name is based
on this pre-existing name. (Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | 3anidm12p2 39958 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜓 ∧ 𝜑 ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
|
Theorem | uun123 39959 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | uun123p1 39960 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | uun123p2 39961 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜒 ∧ 𝜑 ∧ 𝜓) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | uun123p3 39962 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | uun123p4 39963 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
|
Theorem | uun2221 39964 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 30-Dec-2016.)
(Proof modification is discouraged.) (New usage is discouraged.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ∧ 𝜑 ∧ (𝜓 ∧ 𝜑)) → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
|
Theorem | uun2221p1 39965 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ∧ (𝜓 ∧ 𝜑) ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
|
Theorem | uun2221p2 39966 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
(Contributed by Alan Sare, 4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (((𝜓 ∧ 𝜑) ∧ 𝜑 ∧ 𝜑) → 𝜒) ⇒ ⊢ ((𝜓 ∧ 𝜑) → 𝜒) |
|
Theorem | 3impdirp1 39967 |
A deduction unionizing a non-unionized collection of virtual hypotheses.
Commuted version of 3impdir 1413. (Contributed by Alan Sare,
4-Feb-2017.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (((𝜒 ∧ 𝜓) ∧ (𝜑 ∧ 𝜓)) → 𝜃) ⇒ ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜓) → 𝜃) |
|
Theorem | 3impcombi 39968 |
A 1-hypothesis propositional calculus deduction. (Contributed by Alan
Sare, 25-Sep-2017.)
|
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜑) → (𝜒 ↔ 𝜃)) ⇒ ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃) |
|
20.32.6 Theorems proved using Virtual
Deduction
|
|
Theorem | trsspwALT 39969 |
Virtual deduction proof of the left-to-right implication of dftr4 4992. A
transitive class is a subset of its power class. This proof corresponds
to the virtual deduction proof of dftr4 4992 without accumulating results.
(Contributed by Alan Sare, 29-Apr-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) |
|
Theorem | trsspwALT2 39970 |
Virtual deduction proof of trsspwALT 39969. This proof is the same as the
proof of trsspwALT 39969 except each virtual deduction symbol is
replaced by
its non-virtual deduction symbol equivalent. A transitive class is a
subset of its power class. (Contributed by Alan Sare, 23-Jul-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) |
|
Theorem | trsspwALT3 39971 |
Short predicate calculus proof of the left-to-right implication of
dftr4 4992. A transitive class is a subset of its power
class. This
proof was constructed by applying Metamath's minimize command to the
proof of trsspwALT2 39970, which is the virtual deduction proof trsspwALT 39969
without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) |
|
Theorem | sspwtr 39972 |
Virtual deduction proof of the right-to-left implication of dftr4 4992. A
class which is a subclass of its power class is transitive. This proof
corresponds to the virtual deduction proof of sspwtr 39972 without
accumulating results. (Contributed by Alan Sare, 2-May-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
|
Theorem | sspwtrALT 39973 |
Virtual deduction proof of sspwtr 39972. This proof is the same as the
proof of sspwtr 39972 except each virtual deduction symbol is
replaced by
its non-virtual deduction symbol equivalent. A class which is a
subclass of its power class is transitive. (Contributed by Alan Sare,
3-May-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
|
Theorem | sspwtrALT2 39974 |
Short predicate calculus proof of the right-to-left implication of
dftr4 4992. A class which is a subclass of its power
class is transitive.
This proof was constructed by applying Metamath's minimize command to
the proof of sspwtrALT 39973, which is the virtual deduction proof sspwtr 39972
without virtual deductions. (Contributed by Alan Sare, 3-May-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (𝐴 ⊆ 𝒫 𝐴 → Tr 𝐴) |
|
Theorem | pwtrVD 39975 |
Virtual deduction proof of pwtr 5153; see pwtrrVD 39976 for the converse.
(Contributed by Alan Sare, 25-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (Tr 𝐴 → Tr 𝒫 𝐴) |
|
Theorem | pwtrrVD 39976 |
Virtual deduction proof of pwtr 5153; see pwtrVD 39975 for the converse.
(Contributed by Alan Sare, 25-Aug-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ 𝐴 ∈
V ⇒ ⊢ (Tr 𝒫 𝐴 → Tr 𝐴) |
|
Theorem | suctrALT 39977 |
The successor of a transitive class is transitive. The proof of
http://us.metamath.org/other/completeusersproof/suctrvd.html
is a
Virtual Deduction proof verified by automatically transforming it into
the Metamath proof of suctrALT 39977 using completeusersproof, which is
verified by the Metamath program. The proof of
http://us.metamath.org/other/completeusersproof/suctrro.html
is a form
of the completed proof which preserves the Virtual Deduction proof's
step numbers and their ordering. See suctr 6059 for the original proof.
(Contributed by Alan Sare, 11-Apr-2009.) (Revised by Alan Sare,
12-Jun-2018.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (Tr 𝐴 → Tr suc 𝐴) |
|
Theorem | snssiALTVD 39978 |
Virtual deduction proof of snssiALT 39979. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) |
|
Theorem | snssiALT 39979 |
If a class is an element of another class, then its singleton is a
subclass of that other class. Alternate proof of snssi 4570. This
theorem was automatically generated from snssiALTVD 39978 using a
translation program. (Contributed by Alan Sare, 11-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) |
|
Theorem | snsslVD 39980 |
Virtual deduction proof of snssl 39981. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 𝐴 ∈
V ⇒ ⊢ ({𝐴} ⊆ 𝐵 → 𝐴 ∈ 𝐵) |
|
Theorem | snssl 39981 |
If a singleton is a subclass of another class, then the singleton's
element is an element of that other class. This theorem is the
right-to-left implication of the biconditional snss 4548.
The proof of
this theorem was automatically generated from snsslVD 39980 using a tools
command file, translateMWO.cmd, by translating the proof into its
non-virtual deduction form and minimizing it. (Contributed by Alan
Sare, 25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 𝐴 ∈
V ⇒ ⊢ ({𝐴} ⊆ 𝐵 → 𝐴 ∈ 𝐵) |
|
Theorem | snelpwrVD 39982 |
Virtual deduction proof of snelpwi 5144. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵) |
|
Theorem | unipwrVD 39983 |
Virtual deduction proof of unipwr 39984. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 𝐴 ⊆ ∪ 𝒫 𝐴 |
|
Theorem | unipwr 39984 |
A class is a subclass of the union of its power class. This theorem is
the right-to-left subclass lemma of unipw 5150. The proof of this theorem
was automatically generated from unipwrVD 39983 using a tools command file ,
translateMWO.cmd , by translating the proof into its non-virtual
deduction form and minimizing it. (Contributed by Alan Sare,
25-Aug-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ 𝐴 ⊆ ∪ 𝒫 𝐴 |
|
Theorem | sstrALT2VD 39985 |
Virtual deduction proof of sstrALT2 39986. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) |
|
Theorem | sstrALT2 39986 |
Virtual deduction proof of sstr 3828, transitivity of subclasses, Theorem
6 of [Suppes] p. 23. This theorem was
automatically generated from
sstrALT2VD 39985 using the command file translatewithout_overwriting.cmd .
It was not minimized because the automated minimization excluding
duplicates generates a minimized proof which, although not directly
containing any duplicates, indirectly contains a duplicate. That is,
the trace back of the minimized proof contains a duplicate. This is
undesirable because some step(s) of the minimized proof use the proven
theorem. (Contributed by Alan Sare, 11-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶) |
|
Theorem | suctrALT2VD 39987 |
Virtual deduction proof of suctrALT2 39988. (Contributed by Alan Sare,
11-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (Tr 𝐴 → Tr suc 𝐴) |
|
Theorem | suctrALT2 39988 |
Virtual deduction proof of suctr 6059. The sucessor of a transitive class
is transitive. This proof was generated automatically from the virtual
deduction proof suctrALT2VD 39987 using the tools command file
translatewithout_overwritingminimize_excludingduplicates.cmd .
(Contributed by Alan Sare, 11-Sep-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ (Tr 𝐴 → Tr suc 𝐴) |
|
Theorem | elex2VD 39989* |
Virtual deduction proof of elex2 3417. (Contributed by Alan Sare,
25-Sep-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝐴 ∈ 𝐵 → ∃𝑥 𝑥 ∈ 𝐵) |
|
Theorem | elex22VD 39990* |
Virtual deduction proof of elex22 3418. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶) → ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) |
|
Theorem | eqsbc3rVD 39991* |
Virtual deduction proof of eqsbc3r 3710. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝐴 ∈ 𝐵 → ([𝐴 / 𝑥]𝐶 = 𝑥 ↔ 𝐶 = 𝐴)) |
|
Theorem | zfregs2VD 39992* |
Virtual deduction proof of zfregs2 8906. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝐴 ≠ ∅ → ¬
∀𝑥 ∈ 𝐴 ∃𝑦(𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝑥)) |
|
Theorem | tpid3gVD 39993 |
Virtual deduction proof of tpid3g 4538. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ {𝐶, 𝐷, 𝐴}) |
|
Theorem | en3lplem1VD 39994* |
Virtual deduction proof of en3lplem1 8804. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 = 𝐴 → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) |
|
Theorem | en3lplem2VD 39995* |
Virtual deduction proof of en3lplem2 8805. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) → (𝑥 ∈ {𝐴, 𝐵, 𝐶} → ∃𝑦(𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ 𝑦 ∈ 𝑥))) |
|
Theorem | en3lpVD 39996 |
Virtual deduction proof of en3lp 8806. (Contributed by Alan Sare,
24-Oct-2011.) (Proof modification is discouraged.)
(New usage is discouraged.)
|
⊢ ¬ (𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐴) |
|
20.32.7 Theorems proved using Virtual Deduction
with mmj2 assistance
|
|
Theorem | simplbi2VD 39997 |
Virtual deduction proof of simplbi2 496. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
h1:: | ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
| 3:1,?: e0a 39923 | ⊢ ((𝜓 ∧ 𝜒) → 𝜑)
| qed:3,?: e0a 39923 | ⊢ (𝜓 → (𝜒 → 𝜑))
|
The proof of simplbi2 496 was automatically derived from it.
(Contributed by Alan Sare, 31-Dec-2011.) (Proof modification is
discouraged.) (New usage is discouraged.)
|
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 → (𝜒 → 𝜑)) |
|
Theorem | 3ornot23VD 39998 |
Virtual deduction proof of 3ornot23 39651. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) ▶ (¬ 𝜑
∧ ¬ 𝜓) )
| 2:: | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) , (𝜒 ∨ 𝜑
∨ 𝜓) ▶ (𝜒 ∨ 𝜑 ∨ 𝜓) )
| 3:1,?: e1a 39778 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) ▶ ¬ 𝜑 )
| 4:1,?: e1a 39778 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) ▶ ¬ 𝜓 )
| 5:3,4,?: e11 39839 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) ▶ ¬ (𝜑
∨ 𝜓) )
| 6:2,?: e2 39782 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) , (𝜒 ∨ 𝜑
∨ 𝜓) ▶ (𝜒 ∨ (𝜑 ∨ 𝜓)) )
| 7:5,6,?: e12 39875 | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) , (𝜒 ∨ 𝜑
∨ 𝜓) ▶ 𝜒 )
| 8:7: | ⊢ ( (¬ 𝜑 ∧ ¬ 𝜓) ▶ ((𝜒
∨ 𝜑 ∨ 𝜓) → 𝜒) )
| qed:8: | ⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒
∨ 𝜑 ∨ 𝜓) → 𝜒))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((¬ 𝜑 ∧ ¬ 𝜓) → ((𝜒 ∨ 𝜑 ∨ 𝜓) → 𝜒)) |
|
Theorem | orbi1rVD 39999 |
Virtual deduction proof of orbi1r 39652. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: | ⊢ ( (𝜑 ↔ 𝜓) ▶ (𝜑 ↔ 𝜓) )
| 2:: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜑)
▶ (𝜒 ∨ 𝜑) )
| 3:2,?: e2 39782 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜑)
▶ (𝜑 ∨ 𝜒) )
| 4:1,3,?: e12 39875 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜑)
▶ (𝜓 ∨ 𝜒) )
| 5:4,?: e2 39782 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜑)
▶ (𝜒 ∨ 𝜓) )
| 6:5: | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜒 ∨ 𝜑)
→ (𝜒 ∨ 𝜓)) )
| 7:: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜓)
▶ (𝜒 ∨ 𝜓) )
| 8:7,?: e2 39782 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜓)
▶ (𝜓 ∨ 𝜒) )
| 9:1,8,?: e12 39875 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜓)
▶ (𝜑 ∨ 𝜒) )
| 10:9,?: e2 39782 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜒 ∨ 𝜓)
▶ (𝜒 ∨ 𝜑) )
| 11:10: | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜒 ∨ 𝜓)
→ (𝜒 ∨ 𝜑)) )
| 12:6,11,?: e11 39839 | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜒
∨ 𝜑) ↔ (𝜒 ∨ 𝜓)) )
| qed:12: | ⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑)
↔ (𝜒 ∨ 𝜓)))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ↔ 𝜓) → ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))) |
|
Theorem | bitr3VD 40000 |
Virtual deduction proof of bitr3 344. The following user's proof is
completed by invoking mmj2's unify command and using mmj2's StepSelector
to pick all remaining steps of the Metamath proof.
1:: | ⊢ ( (𝜑 ↔ 𝜓) ▶ (𝜑
↔ 𝜓) )
| 2:1,?: e1a 39778 | ⊢ ( (𝜑 ↔ 𝜓) ▶ (𝜓
↔ 𝜑) )
| 3:: | ⊢ ( (𝜑 ↔ 𝜓) , (𝜑 ↔ 𝜒)
▶ (𝜑 ↔ 𝜒) )
| 4:3,?: e2 39782 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜑 ↔ 𝜒)
▶ (𝜒 ↔ 𝜑) )
| 5:2,4,?: e12 39875 | ⊢ ( (𝜑 ↔ 𝜓) , (𝜑 ↔ 𝜒)
▶ (𝜓 ↔ 𝜒) )
| 6:5: | ⊢ ( (𝜑 ↔ 𝜓) ▶ ((𝜑
↔ 𝜒) → (𝜓 ↔ 𝜒)) )
| qed:6: | ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒)
→ (𝜓 ↔ 𝜒)))
|
(Contributed by Alan Sare, 31-Dec-2011.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ↔ 𝜒) → (𝜓 ↔ 𝜒))) |