Users' Mathboxes Mathbox for Andrew Salmon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pm11.71 Structured version   Visualization version   GIF version

Theorem pm11.71 38914
Description: Theorem *11.71 in [WhiteheadRussell] p. 166. (Contributed by Andrew Salmon, 24-May-2011.)
Assertion
Ref Expression
pm11.71 ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → ((∀𝑥(𝜑𝜓) ∧ ∀𝑦(𝜒𝜃)) ↔ ∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃))))
Distinct variable groups:   𝜑,𝑦   𝜓,𝑦   𝜒,𝑥   𝜃,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝜒(𝑦)   𝜃(𝑦)

Proof of Theorem pm11.71
StepHypRef Expression
1 nfv 1883 . . . 4 𝑦(𝜑𝜓)
2 nfv 1883 . . . 4 𝑥(𝜒𝜃)
31, 2aaan 2206 . . 3 (∀𝑥𝑦((𝜑𝜓) ∧ (𝜒𝜃)) ↔ (∀𝑥(𝜑𝜓) ∧ ∀𝑦(𝜒𝜃)))
4 prth 594 . . . 4 (((𝜑𝜓) ∧ (𝜒𝜃)) → ((𝜑𝜒) → (𝜓𝜃)))
542alimi 1780 . . 3 (∀𝑥𝑦((𝜑𝜓) ∧ (𝜒𝜃)) → ∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)))
63, 5sylbir 225 . 2 ((∀𝑥(𝜑𝜓) ∧ ∀𝑦(𝜒𝜃)) → ∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)))
7 nfv 1883 . . . . . 6 𝑥𝜒
87nfex 2192 . . . . 5 𝑥𝑦𝜒
9 exim 1801 . . . . . . 7 (∀𝑦((𝜑𝜒) → (𝜓𝜃)) → (∃𝑦(𝜑𝜒) → ∃𝑦(𝜓𝜃)))
10 19.42v 1921 . . . . . . 7 (∃𝑦(𝜑𝜒) ↔ (𝜑 ∧ ∃𝑦𝜒))
11 19.42v 1921 . . . . . . 7 (∃𝑦(𝜓𝜃) ↔ (𝜓 ∧ ∃𝑦𝜃))
129, 10, 113imtr3g 284 . . . . . 6 (∀𝑦((𝜑𝜒) → (𝜓𝜃)) → ((𝜑 ∧ ∃𝑦𝜒) → (𝜓 ∧ ∃𝑦𝜃)))
13 pm3.21 463 . . . . . . 7 (∃𝑦𝜒 → (𝜑 → (𝜑 ∧ ∃𝑦𝜒)))
14 simpl 472 . . . . . . . 8 ((𝜓 ∧ ∃𝑦𝜃) → 𝜓)
1514imim2i 16 . . . . . . 7 (((𝜑 ∧ ∃𝑦𝜒) → (𝜓 ∧ ∃𝑦𝜃)) → ((𝜑 ∧ ∃𝑦𝜒) → 𝜓))
1613, 15syl9 77 . . . . . 6 (∃𝑦𝜒 → (((𝜑 ∧ ∃𝑦𝜒) → (𝜓 ∧ ∃𝑦𝜃)) → (𝜑𝜓)))
1712, 16syl5 34 . . . . 5 (∃𝑦𝜒 → (∀𝑦((𝜑𝜒) → (𝜓𝜃)) → (𝜑𝜓)))
188, 17alimd 2119 . . . 4 (∃𝑦𝜒 → (∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)) → ∀𝑥(𝜑𝜓)))
1918adantl 481 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → (∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)) → ∀𝑥(𝜑𝜓)))
20 ax-11 2074 . . . . 5 (∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)) → ∀𝑦𝑥((𝜑𝜒) → (𝜓𝜃)))
21 nfv 1883 . . . . . . 7 𝑦𝜑
2221nfex 2192 . . . . . 6 𝑦𝑥𝜑
23 exim 1801 . . . . . . . 8 (∀𝑥((𝜑𝜒) → (𝜓𝜃)) → (∃𝑥(𝜑𝜒) → ∃𝑥(𝜓𝜃)))
24 19.41v 1917 . . . . . . . 8 (∃𝑥(𝜑𝜒) ↔ (∃𝑥𝜑𝜒))
25 19.41v 1917 . . . . . . . 8 (∃𝑥(𝜓𝜃) ↔ (∃𝑥𝜓𝜃))
2623, 24, 253imtr3g 284 . . . . . . 7 (∀𝑥((𝜑𝜒) → (𝜓𝜃)) → ((∃𝑥𝜑𝜒) → (∃𝑥𝜓𝜃)))
27 pm3.2 462 . . . . . . . 8 (∃𝑥𝜑 → (𝜒 → (∃𝑥𝜑𝜒)))
28 simpr 476 . . . . . . . . 9 ((∃𝑥𝜓𝜃) → 𝜃)
2928imim2i 16 . . . . . . . 8 (((∃𝑥𝜑𝜒) → (∃𝑥𝜓𝜃)) → ((∃𝑥𝜑𝜒) → 𝜃))
3027, 29syl9 77 . . . . . . 7 (∃𝑥𝜑 → (((∃𝑥𝜑𝜒) → (∃𝑥𝜓𝜃)) → (𝜒𝜃)))
3126, 30syl5 34 . . . . . 6 (∃𝑥𝜑 → (∀𝑥((𝜑𝜒) → (𝜓𝜃)) → (𝜒𝜃)))
3222, 31alimd 2119 . . . . 5 (∃𝑥𝜑 → (∀𝑦𝑥((𝜑𝜒) → (𝜓𝜃)) → ∀𝑦(𝜒𝜃)))
3320, 32syl5 34 . . . 4 (∃𝑥𝜑 → (∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)) → ∀𝑦(𝜒𝜃)))
3433adantr 480 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → (∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)) → ∀𝑦(𝜒𝜃)))
3519, 34jcad 554 . 2 ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → (∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)) → (∀𝑥(𝜑𝜓) ∧ ∀𝑦(𝜒𝜃))))
366, 35impbid2 216 1 ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → ((∀𝑥(𝜑𝜓) ∧ ∀𝑦(𝜒𝜃)) ↔ ∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  wal 1521  wex 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator