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 1870
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 485 . . . 4 ((𝜑𝜓) → 𝜑)
21alimi 1811 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜑)
3 simpr 487 . . . 4 ((𝜑𝜓) → 𝜓)
43alimi 1811 . . 3 (∀𝑥(𝜑𝜓) → ∀𝑥𝜓)
52, 4jca 514 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ∧ ∀𝑥𝜓))
6 id 22 . . 3 ((𝜑𝜓) → (𝜑𝜓))
76alanimi 1816 . 2 ((∀𝑥𝜑 ∧ ∀𝑥𝜓) → ∀𝑥(𝜑𝜓))
85, 7impbii 211 1 (∀𝑥(𝜑𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398  wal 1534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 209  df-an 399
This theorem is referenced by:  19.26-2  1871  19.26-3an  1872  19.43OLD  1883  albiim  1889  2albiim  1890  19.27v  1995  19.28v  1996  19.27  2228  19.28  2229  r19.26m  3176  unss  4163  ralunb  4170  ssin  4210  falseral0  4462  intun  4911  intpr  4912  eqrelrel  5673  relop  5724  eqoprab2bw  7227  eqoprab2b  7228  dfer2  8293  axgroth4  10257  grothprim  10259  trclfvcotr  14372  caubnd  14721  bj-gl4  33933  bj-nnfand  34082  wl-alanbii  34809  ax12eq  36081  ax12el  36082  dford4  39632  elmapintrab  39942  elinintrab  39943  ismnuprim  40636  alimp-no-surprise  44889
  Copyright terms: Public domain W3C validator