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  4444  intpr  4445  eqrelrel  5144  relop  5194  eqoprab2b  6611  dfer2  7630  axgroth4  9533  grothprim  9535  trclfvcotr  13598  caubnd  13946  bj-gl4lem  31752  bj-gl4  31753  wl-alanbii  32530  ax12eq  33244  ax12el  33245  dford4  36614  elmapintrab  36901  elinintrab  36902  falseral0  40308  alimp-no-surprise  42336
  Copyright terms: Public domain W3C validator