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 1870
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 482 . . . 4 ((𝜑𝜓) → 𝜑)
21alimi 1811 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 484 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1811 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 511 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 22 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1816 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 209 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  wal 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396
This theorem is referenced by:  19.26-2  1871  19.26-3an  1872  19.43OLD  1883  albiim  1889  2albiim  1890  19.27v  1989  19.28v  1990  19.27  2227  19.28  2228  r19.26m  3110  raleqbidvvOLD  3335  unss  4190  ralunb  4197  ssin  4239  falseral0  4516  intun  4980  intprg  4981  eqrelrel  5807  relop  5861  eqoprab2bw  7503  eqoprab2b  7504  dfer2  8746  axgroth4  10872  grothprim  10874  trclfvcotr  15048  caubnd  15397  bj-gl4  36596  bj-nnfand  36750  bj-elgab  36940  wl-alanbii  37570  ax12eq  38942  ax12el  38943  alan  42676  dford4  43041  elmapintrab  43589  elinintrab  43590  ismnuprim  44313  alimp-no-surprise  49300
  Copyright terms: Public domain W3C validator