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 1965
Description: The antecedent provides a condition implying the converse of 19.33 1964. (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 962 . . 3 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 ∨ ¬ ∃𝑥𝜓))
2 alnex 1854 . . . . . 6 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
3 pm2.53 838 . . . . . . 7 ((𝜑𝜓) → (¬ 𝜑𝜓))
43al2imi 1891 . . . . . 6 (∀𝑥(𝜑𝜓) → (∀𝑥 ¬ 𝜑 → ∀𝑥𝜓))
52, 4syl5bir 233 . . . . 5 (∀𝑥(𝜑𝜓) → (¬ ∃𝑥𝜑 → ∀𝑥𝜓))
6 olc 855 . . . . 5 (∀𝑥𝜓 → (∀𝑥𝜑 ∨ ∀𝑥𝜓))
75, 6syl6com 37 . . . 4 (¬ ∃𝑥𝜑 → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
8 19.30 1961 . . . . . . 7 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓))
98orcomd 858 . . . . . 6 (∀𝑥(𝜑𝜓) → (∃𝑥𝜓 ∨ ∀𝑥𝜑))
109ord 851 . . . . 5 (∀𝑥(𝜑𝜓) → (¬ ∃𝑥𝜓 → ∀𝑥𝜑))
11 orc 854 . . . . 5 (∀𝑥𝜑 → (∀𝑥𝜑 ∨ ∀𝑥𝜓))
1210, 11syl6com 37 . . . 4 (¬ ∃𝑥𝜓 → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
137, 12jaoi 844 . . 3 ((¬ ∃𝑥𝜑 ∨ ¬ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
141, 13sylbi 207 . 2 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
15 19.33 1964 . 2 ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
1614, 15impbid1 215 1 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  wo 834  wal 1629  wex 1852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-ex 1853
This theorem is referenced by:  kmlem16  9189
  Copyright terms: Public domain W3C validator