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

Theorem 19.26 1838
Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 147. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
Assertion
Ref Expression
19.26 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))

Proof of Theorem 19.26
StepHypRef Expression
1 simpl 472 . . . 4 ((𝜑𝜓) → 𝜑)
21alimi 1779 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 476 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1779 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 553 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 22 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1784 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 199 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wal 1521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  19.26-2  1839  19.26-3an  1840  19.43OLD  1851  albiim  1856  2albiim  1857  19.27v  1964  19.28v  1965  19.27  2133  19.28  2134  19.27OLD  2270  19.28OLD  2271  r19.26m  3096  unss  3820  ralunb  3827  ssin  3868  falseral0  4114  intun  4541  intpr  4542  eqrelrel  5255  relop  5305  eqoprab2b  6755  dfer2  7788  axgroth4  9692  grothprim  9694  trclfvcotr  13794  caubnd  14142  bj-gl4lem  32704  bj-gl4  32705  wl-alanbii  33481  ax12eq  34545  ax12el  34546  dford4  37913  elmapintrab  38199  elinintrab  38200  alimp-no-surprise  42855
  Copyright terms: Public domain W3C validator