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

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

Proof of Theorem bj-cbvalimt
StepHypRef Expression
1 exim 1830 . . 3 (∀𝑥(𝜒 → (𝜑𝜓)) → (∃𝑥𝜒 → ∃𝑥(𝜑𝜓)))
21al2imi 1812 . 2 (∀𝑦𝑥(𝜒 → (𝜑𝜓)) → (∀𝑦𝑥𝜒 → ∀𝑦𝑥(𝜑𝜓)))
3 pm2.27 42 . . . . . 6 (𝜑 → ((𝜑𝜓) → 𝜓))
43aleximi 1828 . . . . 5 (∀𝑥𝜑 → (∃𝑥(𝜑𝜓) → ∃𝑥𝜓))
54com12 32 . . . 4 (∃𝑥(𝜑𝜓) → (∀𝑥𝜑 → ∃𝑥𝜓))
65alimi 1808 . . 3 (∀𝑦𝑥(𝜑𝜓) → ∀𝑦(∀𝑥𝜑 → ∃𝑥𝜓))
7 alim 1807 . . 3 (∀𝑦(∀𝑥𝜑 → ∃𝑥𝜓) → (∀𝑦𝑥𝜑 → ∀𝑦𝑥𝜓))
8 alim 1807 . . . . 5 (∀𝑦(∃𝑥𝜓𝜓) → (∀𝑦𝑥𝜓 → ∀𝑦𝜓))
9 imim1 83 . . . . 5 ((∀𝑦𝑥𝜑 → ∀𝑦𝑥𝜓) → ((∀𝑦𝑥𝜓 → ∀𝑦𝜓) → (∀𝑦𝑥𝜑 → ∀𝑦𝜓)))
10 imim2 58 . . . . 5 ((∀𝑦𝑥𝜑 → ∀𝑦𝜓) → ((∀𝑥𝜑 → ∀𝑦𝑥𝜑) → (∀𝑥𝜑 → ∀𝑦𝜓)))
118, 9, 10syl56 36 . . . 4 ((∀𝑦𝑥𝜑 → ∀𝑦𝑥𝜓) → (∀𝑦(∃𝑥𝜓𝜓) → ((∀𝑥𝜑 → ∀𝑦𝑥𝜑) → (∀𝑥𝜑 → ∀𝑦𝜓))))
1211com23 86 . . 3 ((∀𝑦𝑥𝜑 → ∀𝑦𝑥𝜓) → ((∀𝑥𝜑 → ∀𝑦𝑥𝜑) → (∀𝑦(∃𝑥𝜓𝜓) → (∀𝑥𝜑 → ∀𝑦𝜓))))
136, 7, 123syl 18 . 2 (∀𝑦𝑥(𝜑𝜓) → ((∀𝑥𝜑 → ∀𝑦𝑥𝜑) → (∀𝑦(∃𝑥𝜓𝜓) → (∀𝑥𝜑 → ∀𝑦𝜓))))
142, 13syl6com 37 1 (∀𝑦𝑥𝜒 → (∀𝑦𝑥(𝜒 → (𝜑𝜓)) → ((∀𝑥𝜑 → ∀𝑦𝑥𝜑) → (∀𝑦(∃𝑥𝜓𝜓) → (∀𝑥𝜑 → ∀𝑦𝜓)))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1531  ∃wex 1776 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806 This theorem depends on definitions:  df-bi 209  df-ex 1777 This theorem is referenced by:  bj-cbvalim  33978
 Copyright terms: Public domain W3C validator