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 1796
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 473 . . . 4 ((𝜑𝜓) → 𝜑)
21alimi 1737 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 477 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1737 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 554 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 22 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1742 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 199 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wal 1479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  19.26-2  1797  19.26-3an  1798  19.43OLD  1809  albiim  1814  2albiim  1815  19.27v  1906  19.28v  1907  19.27  2093  19.28  2094  19.27OLD  2232  19.28OLD  2233  r19.26m  3063  unss  3779  ralunb  3786  ssin  3827  falseral0  4072  intun  4500  intpr  4501  eqrelrel  5211  relop  5261  eqoprab2b  6698  dfer2  7728  axgroth4  9639  grothprim  9641  trclfvcotr  13731  caubnd  14079  bj-gl4lem  32554  bj-gl4  32555  wl-alanbii  33322  ax12eq  34045  ax12el  34046  dford4  37415  elmapintrab  37701  elinintrab  37702  alimp-no-surprise  42292
  Copyright terms: Public domain W3C validator