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 1866
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 481 . . . 4 ((𝜑𝜓) → 𝜑)
21alimi 1806 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 483 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1806 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 510 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 22 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1811 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 208 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  wal 1532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804
This theorem depends on definitions:  df-bi 206  df-an 395
This theorem is referenced by:  19.26-2  1867  19.26-3an  1868  19.43OLD  1879  albiim  1885  2albiim  1886  19.27v  1986  19.28v  1987  19.27  2216  19.28  2217  r19.26m  3100  raleqbidvvOLD  3320  unss  4182  ralunb  4189  ssin  4229  falseral0  4514  intun  4980  intprg  4981  intprOLD  4983  eqrelrel  5795  relop  5849  eqoprab2bw  7487  eqoprab2b  7488  dfer2  8727  axgroth4  10866  grothprim  10868  trclfvcotr  15009  caubnd  15358  bj-gl4  36313  bj-nnfand  36467  bj-elgab  36658  wl-alanbii  37277  ax12eq  38652  ax12el  38653  dford4  42724  elmapintrab  43280  elinintrab  43281  ismnuprim  44005  alimp-no-surprise  48565
  Copyright terms: Public domain W3C validator