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 1948
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 468 . . . 4 ((𝜑𝜓) → 𝜑)
21alimi 1886 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 471 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1886 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 495 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 22 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1891 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 199 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382  wal 1628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884
This theorem depends on definitions:  df-bi 197  df-an 383
This theorem is referenced by:  19.26-2  1949  19.26-3an  1950  19.26-3anOLD  1951  19.43OLD  1962  albiim  1967  2albiim  1968  19.27v  2075  19.28v  2076  19.27  2250  19.28  2251  19.27OLD  2395  19.28OLD  2396  r19.26m  3214  unss  3936  ralunb  3943  ssin  3981  falseral0  4218  intun  4641  intpr  4642  eqrelrel  5361  relop  5411  eqoprab2b  6859  dfer2  7896  axgroth4  9855  grothprim  9857  trclfvcotr  13957  caubnd  14305  bj-gl4lem  32910  bj-gl4  32911  wl-alanbii  33678  ax12eq  34742  ax12el  34743  dford4  38115  elmapintrab  38401  elinintrab  38402  alimp-no-surprise  43048
  Copyright terms: Public domain W3C validator