Metamath Proof Explorer


Theorem bj-exlimd

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 ( 𝜑 → ( ∃ 𝑥 𝜒𝜏 ) )