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 1972
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 476 . . . 4 ((𝜑𝜓) → 𝜑)
21alimi 1910 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 479 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1910 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 507 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 22 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1915 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 201 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 386  wal 1654
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908
This theorem depends on definitions:  df-bi 199  df-an 387
This theorem is referenced by:  19.26-2  1973  19.26-3an  1974  19.26-3anOLD  1975  19.43OLD  1986  albiim  1991  2albiim  1992  19.27v  2094  19.28v  2095  19.27  2270  19.28  2271  eu6OLD  2647  r19.26m  3277  unss  4016  ralunb  4023  ssin  4061  falseral0  4303  intun  4731  intpr  4732  eqrelrel  5459  relop  5509  eqoprab2b  6978  dfer2  8015  axgroth4  9976  grothprim  9978  trclfvcotr  14134  caubnd  14482  bj-gl4lem  33103  bj-gl4  33104  wl-alanbii  33894  ax12eq  35015  ax12el  35016  dford4  38438  elmapintrab  38722  elinintrab  38723  alimp-no-surprise  43437
  Copyright terms: Public domain W3C validator