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