Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.33b Structured version   Visualization version   GIF version

Theorem 19.33b 1886
 Description: The antecedent provides a condition implying the converse of 19.33 1885. (Contributed by NM, 27-Mar-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 5-Jul-2014.)
Assertion
Ref Expression
19.33b (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓)))

Proof of Theorem 19.33b
StepHypRef Expression
1 ianor 979 . . 3 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 ∨ ¬ ∃𝑥𝜓))
2 alnex 1783 . . . . . 6 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
3 pm2.53 848 . . . . . . 7 ((𝜑𝜓) → (¬ 𝜑𝜓))
43al2imi 1817 . . . . . 6 (∀𝑥(𝜑𝜓) → (∀𝑥 ¬ 𝜑 → ∀𝑥𝜓))
52, 4syl5bir 246 . . . . 5 (∀𝑥(𝜑𝜓) → (¬ ∃𝑥𝜑 → ∀𝑥𝜓))
6 olc 865 . . . . 5 (∀𝑥𝜓 → (∀𝑥𝜑 ∨ ∀𝑥𝜓))
75, 6syl6com 37 . . . 4 (¬ ∃𝑥𝜑 → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
8 19.30 1882 . . . . . . 7 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓))
98orcomd 868 . . . . . 6 (∀𝑥(𝜑𝜓) → (∃𝑥𝜓 ∨ ∀𝑥𝜑))
109ord 861 . . . . 5 (∀𝑥(𝜑𝜓) → (¬ ∃𝑥𝜓 → ∀𝑥𝜑))
11 orc 864 . . . . 5 (∀𝑥𝜑 → (∀𝑥𝜑 ∨ ∀𝑥𝜓))
1210, 11syl6com 37 . . . 4 (¬ ∃𝑥𝜓 → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
137, 12jaoi 854 . . 3 ((¬ ∃𝑥𝜑 ∨ ¬ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
141, 13sylbi 220 . 2 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
15 19.33 1885 . 2 ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
1614, 15impbid1 228 1 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844  ∀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-an 400  df-or 845  df-ex 1782 This theorem is referenced by:  kmlem16  9583
 Copyright terms: Public domain W3C validator