Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Adding ax-4
bj-exlimd
Metamath Proof Explorer
Description: A slightly more general exlimd . A common usage will have ph
substituted for ps and th substituted for ta , giving a form
closer to exlimd . (Contributed by BJ , 25-Dec-2023)
Ref
Expression
Hypotheses
bj-exlimd.ph
⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
bj-exlimd.th
⊢ ( 𝜑 → ( ∃ 𝑥 𝜃 → 𝜏 ) )
bj-exlimd.maj
⊢ ( 𝜓 → ( 𝜒 → 𝜃 ) )
Assertion
bj-exlimd
⊢ ( 𝜑 → ( ∃ 𝑥 𝜒 → 𝜏 ) )
Proof
Step
Hyp
Ref
Expression
1
bj-exlimd.ph
⊢ ( 𝜑 → ∀ 𝑥 𝜓 )
2
bj-exlimd.th
⊢ ( 𝜑 → ( ∃ 𝑥 𝜃 → 𝜏 ) )
3
bj-exlimd.maj
⊢ ( 𝜓 → ( 𝜒 → 𝜃 ) )
4
1 3
sylg
⊢ ( 𝜑 → ∀ 𝑥 ( 𝜒 → 𝜃 ) )
5
bj-exlimg
⊢ ( ( ∃ 𝑥 𝜃 → 𝜏 ) → ( ∀ 𝑥 ( 𝜒 → 𝜃 ) → ( ∃ 𝑥 𝜒 → 𝜏 ) ) )
6
2 4 5
sylc
⊢ ( 𝜑 → ( ∃ 𝑥 𝜒 → 𝜏 ) )