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 1984
Description: The antecedent provides a condition implying the converse of 19.33 1983. (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 1004 . . 3 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) ↔ (¬ ∃𝑥𝜑 ∨ ¬ ∃𝑥𝜓))
2 alnex 1876 . . . . . 6 (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
3 pm2.53 877 . . . . . . 7 ((𝜑𝜓) → (¬ 𝜑𝜓))
43al2imi 1910 . . . . . 6 (∀𝑥(𝜑𝜓) → (∀𝑥 ¬ 𝜑 → ∀𝑥𝜓))
52, 4syl5bir 234 . . . . 5 (∀𝑥(𝜑𝜓) → (¬ ∃𝑥𝜑 → ∀𝑥𝜓))
6 olc 894 . . . . 5 (∀𝑥𝜓 → (∀𝑥𝜑 ∨ ∀𝑥𝜓))
75, 6syl6com 37 . . . 4 (¬ ∃𝑥𝜑 → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
8 19.30 1980 . . . . . . 7 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∃𝑥𝜓))
98orcomd 897 . . . . . 6 (∀𝑥(𝜑𝜓) → (∃𝑥𝜓 ∨ ∀𝑥𝜑))
109ord 890 . . . . 5 (∀𝑥(𝜑𝜓) → (¬ ∃𝑥𝜓 → ∀𝑥𝜑))
11 orc 893 . . . . 5 (∀𝑥𝜑 → (∀𝑥𝜑 ∨ ∀𝑥𝜓))
1210, 11syl6com 37 . . . 4 (¬ ∃𝑥𝜓 → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
137, 12jaoi 883 . . 3 ((¬ ∃𝑥𝜑 ∨ ¬ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
141, 13sylbi 208 . 2 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
15 19.33 1983 . 2 ((∀𝑥𝜑 ∨ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
1614, 15impbid1 216 1 (¬ (∃𝑥𝜑 ∧ ∃𝑥𝜓) → (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∨ ∀𝑥𝜓)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  wal 1650  wex 1874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-ex 1875
This theorem is referenced by:  kmlem16  9240
  Copyright terms: Public domain W3C validator