Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-cbveximt Structured version   Visualization version   GIF version

Theorem bj-cbveximt 34047
Description: A lemma in closed form used to prove bj-cbvex 34057 in a weak axiomatization. (Contributed by BJ, 12-Mar-2023.) Do not use 19.35 1878 since only the direction of the biconditional used here holds in intuitionistic logic. (Proof modification is discouraged.)
Assertion
Ref Expression
bj-cbveximt (∀𝑥𝑦𝜒 → (∀𝑥𝑦(𝜒 → (𝜑𝜓)) → (∀𝑥(𝜑 → ∀𝑦𝜑) → ((∃𝑥𝑦𝜓 → ∃𝑦𝜓) → (∃𝑥𝜑 → ∃𝑦𝜓)))))

Proof of Theorem bj-cbveximt
StepHypRef Expression
1 bj-exalim 34039 . . . 4 (∀𝑦(𝜒 → (𝜑𝜓)) → (∃𝑦𝜒 → (∀𝑦𝜑 → ∃𝑦𝜓)))
21alimi 1813 . . 3 (∀𝑥𝑦(𝜒 → (𝜑𝜓)) → ∀𝑥(∃𝑦𝜒 → (∀𝑦𝜑 → ∃𝑦𝜓)))
3 bj-alexim 34034 . . 3 (∀𝑥(∃𝑦𝜒 → (∀𝑦𝜑 → ∃𝑦𝜓)) → (∀𝑥𝑦𝜒 → (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)))
42, 3syl 17 . 2 (∀𝑥𝑦(𝜒 → (𝜑𝜓)) → (∀𝑥𝑦𝜒 → (∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓)))
5 exim 1835 . . 3 (∀𝑥(𝜑 → ∀𝑦𝜑) → (∃𝑥𝜑 → ∃𝑥𝑦𝜑))
6 imim2 58 . . 3 ((∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓) → ((∃𝑥𝜑 → ∃𝑥𝑦𝜑) → (∃𝑥𝜑 → ∃𝑥𝑦𝜓)))
7 imim1 83 . . 3 ((∃𝑥𝜑 → ∃𝑥𝑦𝜓) → ((∃𝑥𝑦𝜓 → ∃𝑦𝜓) → (∃𝑥𝜑 → ∃𝑦𝜓)))
85, 6, 7syl56 36 . 2 ((∃𝑥𝑦𝜑 → ∃𝑥𝑦𝜓) → (∀𝑥(𝜑 → ∀𝑦𝜑) → ((∃𝑥𝑦𝜓 → ∃𝑦𝜓) → (∃𝑥𝜑 → ∃𝑦𝜓))))
94, 8syl6com 37 1 (∀𝑥𝑦𝜒 → (∀𝑥𝑦(𝜒 → (𝜑𝜓)) → (∀𝑥(𝜑 → ∀𝑦𝜑) → ((∃𝑥𝑦𝜓 → ∃𝑦𝜓) → (∃𝑥𝜑 → ∃𝑦𝜓)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1536  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-ex 1782
This theorem is referenced by:  bj-cbvexim  34053
  Copyright terms: Public domain W3C validator