MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.26 Structured version   Unicode version

Theorem 19.26 1657
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  |-  ( A. x ( ph  /\  ps )  <->  ( A. x ph  /\  A. x ps ) )

Proof of Theorem 19.26
StepHypRef Expression
1 simpl 457 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21alimi 1614 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ph )
3 simpr 461 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43alimi 1614 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ps )
52, 4jca 532 . 2  |-  ( A. x ( ph  /\  ps )  ->  ( A. x ph  /\  A. x ps ) )
6 id 22 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ps ) )
76alanimi 1617 . 2  |-  ( ( A. x ph  /\  A. x ps )  ->  A. x ( ph  /\  ps ) )
85, 7impbii 188 1  |-  ( A. x ( ph  /\  ps )  <->  ( A. x ph  /\  A. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   A.wal 1377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  19.26-2  1658  19.26-3an  1659  19.35OLD  1665  19.43OLD  1671  albiim  1675  2albiim  1676  19.27  1870  19.28  1871  ax12eq  2264  ax12el  2265  2eu4OLD  2391  bm1.1OLD  2451  r19.26m  2997  unss  3683  ralunb  3690  ssin  3725  intun  4320  intpr  4321  eqrelrel  5110  relop  5159  eqoprab2b  6350  dfer2  7324  axgroth4  9222  grothprim  9224  caubnd  13171  wl-alanbii  29945  dford4  30899  alimp-no-surprise  32678  bj-gl4lem  33666  bj-gl4  33667
  Copyright terms: Public domain W3C validator