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 37402
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 1829 . . . 4 𝑦(𝜑𝜓)
2 nfv 1829 . . . 4 𝑥(𝜒𝜃)
31, 2aaan 2155 . . 3 (∀𝑥𝑦((𝜑𝜓) ∧ (𝜒𝜃)) ↔ (∀𝑥(𝜑𝜓) ∧ ∀𝑦(𝜒𝜃)))
4 prth 592 . . . 4 (((𝜑𝜓) ∧ (𝜒𝜃)) → ((𝜑𝜒) → (𝜓𝜃)))
542alimi 1730 . . 3 (∀𝑥𝑦((𝜑𝜓) ∧ (𝜒𝜃)) → ∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)))
63, 5sylbir 223 . 2 ((∀𝑥(𝜑𝜓) ∧ ∀𝑦(𝜒𝜃)) → ∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)))
7 nfv 1829 . . . . . 6 𝑥𝜒
87nfex 2139 . . . . 5 𝑥𝑦𝜒
9 exim 1750 . . . . . . 7 (∀𝑦((𝜑𝜒) → (𝜓𝜃)) → (∃𝑦(𝜑𝜒) → ∃𝑦(𝜓𝜃)))
10 19.42v 1904 . . . . . . 7 (∃𝑦(𝜑𝜒) ↔ (𝜑 ∧ ∃𝑦𝜒))
11 19.42v 1904 . . . . . . 7 (∃𝑦(𝜓𝜃) ↔ (𝜓 ∧ ∃𝑦𝜃))
129, 10, 113imtr3g 282 . . . . . 6 (∀𝑦((𝜑𝜒) → (𝜓𝜃)) → ((𝜑 ∧ ∃𝑦𝜒) → (𝜓 ∧ ∃𝑦𝜃)))
13 pm3.21 462 . . . . . . 7 (∃𝑦𝜒 → (𝜑 → (𝜑 ∧ ∃𝑦𝜒)))
14 simpl 471 . . . . . . . 8 ((𝜓 ∧ ∃𝑦𝜃) → 𝜓)
1514imim2i 16 . . . . . . 7 (((𝜑 ∧ ∃𝑦𝜒) → (𝜓 ∧ ∃𝑦𝜃)) → ((𝜑 ∧ ∃𝑦𝜒) → 𝜓))
1613, 15syl9 74 . . . . . 6 (∃𝑦𝜒 → (((𝜑 ∧ ∃𝑦𝜒) → (𝜓 ∧ ∃𝑦𝜃)) → (𝜑𝜓)))
1712, 16syl5 33 . . . . 5 (∃𝑦𝜒 → (∀𝑦((𝜑𝜒) → (𝜓𝜃)) → (𝜑𝜓)))
188, 17alimd 2067 . . . 4 (∃𝑦𝜒 → (∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)) → ∀𝑥(𝜑𝜓)))
1918adantl 480 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → (∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)) → ∀𝑥(𝜑𝜓)))
20 ax-11 2020 . . . . 5 (∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)) → ∀𝑦𝑥((𝜑𝜒) → (𝜓𝜃)))
21 nfv 1829 . . . . . . 7 𝑦𝜑
2221nfex 2139 . . . . . 6 𝑦𝑥𝜑
23 exim 1750 . . . . . . . 8 (∀𝑥((𝜑𝜒) → (𝜓𝜃)) → (∃𝑥(𝜑𝜒) → ∃𝑥(𝜓𝜃)))
24 19.41v 1900 . . . . . . . 8 (∃𝑥(𝜑𝜒) ↔ (∃𝑥𝜑𝜒))
25 19.41v 1900 . . . . . . . 8 (∃𝑥(𝜓𝜃) ↔ (∃𝑥𝜓𝜃))
2623, 24, 253imtr3g 282 . . . . . . 7 (∀𝑥((𝜑𝜒) → (𝜓𝜃)) → ((∃𝑥𝜑𝜒) → (∃𝑥𝜓𝜃)))
27 pm3.2 461 . . . . . . . 8 (∃𝑥𝜑 → (𝜒 → (∃𝑥𝜑𝜒)))
28 simpr 475 . . . . . . . . 9 ((∃𝑥𝜓𝜃) → 𝜃)
2928imim2i 16 . . . . . . . 8 (((∃𝑥𝜑𝜒) → (∃𝑥𝜓𝜃)) → ((∃𝑥𝜑𝜒) → 𝜃))
3027, 29syl9 74 . . . . . . 7 (∃𝑥𝜑 → (((∃𝑥𝜑𝜒) → (∃𝑥𝜓𝜃)) → (𝜒𝜃)))
3126, 30syl5 33 . . . . . 6 (∃𝑥𝜑 → (∀𝑥((𝜑𝜒) → (𝜓𝜃)) → (𝜒𝜃)))
3222, 31alimd 2067 . . . . 5 (∃𝑥𝜑 → (∀𝑦𝑥((𝜑𝜒) → (𝜓𝜃)) → ∀𝑦(𝜒𝜃)))
3320, 32syl5 33 . . . 4 (∃𝑥𝜑 → (∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)) → ∀𝑦(𝜒𝜃)))
3433adantr 479 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → (∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)) → ∀𝑦(𝜒𝜃)))
3519, 34jcad 553 . 2 ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → (∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃)) → (∀𝑥(𝜑𝜓) ∧ ∀𝑦(𝜒𝜃))))
366, 35impbid2 214 1 ((∃𝑥𝜑 ∧ ∃𝑦𝜒) → ((∀𝑥(𝜑𝜓) ∧ ∀𝑦(𝜒𝜃)) ↔ ∀𝑥𝑦((𝜑𝜒) → (𝜓𝜃))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  wal 1472  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ex 1695  df-nf 1700
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator