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

Theorem 19.33b 1810
 Description: The antecedent provides a condition implying the converse of 19.33 1809. (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 509 . . 3 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 ∨ ¬ ∃𝑥𝜓))
2 alnex 1703 . . . . . 6 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
3 pm2.53 388 . . . . . . 7 ((𝜑𝜓) → (¬ 𝜑𝜓))
43al2imi 1740 . . . . . 6 (∀𝑥(𝜑𝜓) → (∀𝑥 ¬ 𝜑 → ∀𝑥𝜓))
52, 4syl5bir 233 . . . . 5 (∀𝑥(𝜑𝜓) → (¬ ∃𝑥𝜑 → ∀𝑥𝜓))
6 olc 399 . . . . 5 (∀𝑥𝜓 → (∀𝑥𝜑 ∨ ∀𝑥𝜓))
75, 6syl6com 37 . . . 4 (¬ ∃𝑥𝜑 → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
8 19.30 1806 . . . . . . 7 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓))
98orcomd 403 . . . . . 6 (∀𝑥(𝜑𝜓) → (∃𝑥𝜓 ∨ ∀𝑥𝜑))
109ord 392 . . . . 5 (∀𝑥(𝜑𝜓) → (¬ ∃𝑥𝜓 → ∀𝑥𝜑))
11 orc 400 . . . . 5 (∀𝑥𝜑 → (∀𝑥𝜑 ∨ ∀𝑥𝜓))
1210, 11syl6com 37 . . . 4 (¬ ∃𝑥𝜓 → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
137, 12jaoi 394 . . 3 ((¬ ∃𝑥𝜑 ∨ ¬ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
141, 13sylbi 207 . 2 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
15 19.33 1809 . 2 ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
1614, 15impbid1 215 1 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384  ∀wal 1478  ∃wex 1701 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702 This theorem is referenced by:  kmlem16  8939
 Copyright terms: Public domain W3C validator