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

Theorem 19.26 1592
Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 147. (Contributed by NM, 5-Aug-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 445 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21alimi 1546 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ph )
3 simpr 449 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43alimi 1546 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ps )
52, 4jca 520 . 2  |-  ( A. x ( ph  /\  ps )  ->  ( A. x ph  /\  A. x ps ) )
6 id 21 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ps ) )
76alanimi 1550 . 2  |-  ( ( A. x ph  /\  A. x ps )  ->  A. x ( ph  /\  ps ) )
85, 7impbii 182 1  |-  ( A. x ( ph  /\  ps )  <->  ( A. x ph  /\  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360   A.wal 1532
This theorem is referenced by:  19.26-2  1593  19.26-3an  1594  19.35  1599  19.43OLD  1605  albiim  1612  2albiim  1613  ax12olem22  1656  19.27  1786  19.28  1787  ax11eq  2108  ax11el  2109  2eu4  2199  bm1.1  2241  r19.26m  2649  unss  3291  ralunb  3298  ssin  3333  intun  3835  intpr  3836  eqrelrel  4741  relop  4787  eqoprab2b  5805  dfer2  6594  axgroth4  8387  grothprim  8389  caubnd  11772  pgapspf2  25385  dford4  26454  equextvK  28203  ax12olem22K  28204  ax12olem22X  28205  a12stdy2-x12  28242  a12study4  28247  a12stdy2  28257
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator