Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Adding ax-4
bj-sylgt2
Next ⟩
bj-alrimg
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-sylgt2
Description:
Uncurried (imported) form of
sylgt
.
(Contributed by
BJ
, 2-May-2019)
Ref
Expression
Assertion
bj-sylgt2
⊢
∀
x
ψ
→
χ
∧
φ
→
∀
x
ψ
→
φ
→
∀
x
χ
Proof
Step
Hyp
Ref
Expression
1
sylgt
⊢
∀
x
ψ
→
χ
→
φ
→
∀
x
ψ
→
φ
→
∀
x
χ
2
1
imp
⊢
∀
x
ψ
→
χ
∧
φ
→
∀
x
ψ
→
φ
→
∀
x
χ