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  2651  unss  3310  ralunb  3317  ssin  3352  intun  3854  intpr  3855  eqrelrel  4762  relop  4808  eqoprab2b  5826  dfer2  6615  axgroth4  8408  grothprim  8410  caubnd  11793  pgapspf2  25406  dford4  26475  equextvK  28224  ax12olem22K  28225  ax12olem22X  28226  a12stdy2-x12  28263  a12study4  28268  a12stdy2  28278
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