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

Theorem 19.33b 1848
Description: The antecedent provides a condition implying the converse of 19.33 1847. (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 964 . . 3 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 ∨ ¬ ∃𝑥𝜓))
2 alnex 1744 . . . . . 6 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
3 pm2.53 837 . . . . . . 7 ((𝜑𝜓) → (¬ 𝜑𝜓))
43al2imi 1778 . . . . . 6 (∀𝑥(𝜑𝜓) → (∀𝑥 ¬ 𝜑 → ∀𝑥𝜓))
52, 4syl5bir 235 . . . . 5 (∀𝑥(𝜑𝜓) → (¬ ∃𝑥𝜑 → ∀𝑥𝜓))
6 olc 854 . . . . 5 (∀𝑥𝜓 → (∀𝑥𝜑 ∨ ∀𝑥𝜓))
75, 6syl6com 37 . . . 4 (¬ ∃𝑥𝜑 → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
8 19.30 1844 . . . . . . 7 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓))
98orcomd 857 . . . . . 6 (∀𝑥(𝜑𝜓) → (∃𝑥𝜓 ∨ ∀𝑥𝜑))
109ord 850 . . . . 5 (∀𝑥(𝜑𝜓) → (¬ ∃𝑥𝜓 → ∀𝑥𝜑))
11 orc 853 . . . . 5 (∀𝑥𝜑 → (∀𝑥𝜑 ∨ ∀𝑥𝜓))
1210, 11syl6com 37 . . . 4 (¬ ∃𝑥𝜓 → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
137, 12jaoi 843 . . 3 ((¬ ∃𝑥𝜑 ∨ ¬ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
141, 13sylbi 209 . 2 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
15 19.33 1847 . 2 ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
1614, 15impbid1 217 1 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  wo 833  wal 1505  wex 1742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-ex 1743
This theorem is referenced by:  kmlem16  9385
  Copyright terms: Public domain W3C validator