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 1786
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 472 . . . 4 ((𝜑𝜓) → 𝜑)
21alimi 1730 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 476 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1730 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 553 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 22 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1734 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 198 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383  wal 1473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728
This theorem depends on definitions:  df-bi 196  df-an 385
This theorem is referenced by:  19.26-2  1787  19.26-3an  1788  19.43OLD  1800  albiim  1806  2albiim  1807  19.27v  1895  19.28v  1896  19.27  2082  19.28  2083  19.27OLD  2222  19.28OLD  2223  r19.26m  3049  unss  3749  ralunb  3756  ssin  3797  intun  4439  intpr  4440  eqrelrel  5133  relop  5182  eqoprab2b  6589  dfer2  7608  axgroth4  9511  grothprim  9513  trclfvcotr  13547  caubnd  13895  bj-gl4lem  31546  bj-gl4  31547  wl-alanbii  32324  ax12eq  33038  ax12el  33039  dford4  36408  elmapintrab  36695  elinintrab  36696  falseral0  40103  alimp-no-surprise  42289
  Copyright terms: Public domain W3C validator