Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Adding ax-4
bj-sylget
Next ⟩
bj-sylget2
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-sylget
Description:
Dual statement of
sylgt
. Closed form of
bj-sylge
.
(Contributed by
BJ
, 2-May-2019)
Ref
Expression
Assertion
bj-sylget
⊢
∀
x
χ
→
φ
→
∃
x
φ
→
ψ
→
∃
x
χ
→
ψ
Proof
Step
Hyp
Ref
Expression
1
exim
⊢
∀
x
χ
→
φ
→
∃
x
χ
→
∃
x
φ
2
1
imim1d
⊢
∀
x
χ
→
φ
→
∃
x
φ
→
ψ
→
∃
x
χ
→
ψ