Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  r19.30OLD Structured version   Visualization version   GIF version

Theorem r19.30OLD 3300
 Description: Obsolete version of r19.30 3299 as of 18-Jun-2023. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
r19.30OLD (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓))

Proof of Theorem r19.30OLD
StepHypRef Expression
1 ralim 3129 . 2 (∀𝑥𝐴𝜓𝜑) → (∀𝑥𝐴 ¬ 𝜓 → ∀𝑥𝐴 𝜑))
2 orcom 865 . . . 4 ((𝜑𝜓) ↔ (𝜓𝜑))
3 df-or 843 . . . 4 ((𝜓𝜑) ↔ (¬ 𝜓𝜑))
42, 3bitri 276 . . 3 ((𝜑𝜓) ↔ (¬ 𝜓𝜑))
54ralbii 3132 . 2 (∀𝑥𝐴 (𝜑𝜓) ↔ ∀𝑥𝐴𝜓𝜑))
6 orcom 865 . . 3 ((∀𝑥𝐴 𝜑 ∨ ¬ ∀𝑥𝐴 ¬ 𝜓) ↔ (¬ ∀𝑥𝐴 ¬ 𝜓 ∨ ∀𝑥𝐴 𝜑))
7 dfrex2 3203 . . . 4 (∃𝑥𝐴 𝜓 ↔ ¬ ∀𝑥𝐴 ¬ 𝜓)
87orbi2i 907 . . 3 ((∀𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓) ↔ (∀𝑥𝐴 𝜑 ∨ ¬ ∀𝑥𝐴 ¬ 𝜓))
9 imor 848 . . 3 ((∀𝑥𝐴 ¬ 𝜓 → ∀𝑥𝐴 𝜑) ↔ (¬ ∀𝑥𝐴 ¬ 𝜓 ∨ ∀𝑥𝐴 𝜑))
106, 8, 93bitr4i 304 . 2 ((∀𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓) ↔ (∀𝑥𝐴 ¬ 𝜓 → ∀𝑥𝐴 𝜑))
111, 5, 103imtr4i 293 1 (∀𝑥𝐴 (𝜑𝜓) → (∀𝑥𝐴 𝜑 ∨ ∃𝑥𝐴 𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 842  ∀wral 3105  ∃wrex 3106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-ex 1762  df-ral 3110  df-rex 3111 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator