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

Theorem 19.26 1580
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 443 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21alimi 1546 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ph )
3 simpr 447 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43alimi 1546 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ps )
52, 4jca 518 . 2  |-  ( A. x ( ph  /\  ps )  ->  ( A. x ph  /\  A. x ps ) )
6 id 19 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ps ) )
76alanimi 1549 . 2  |-  ( ( A. x ph  /\  A. x ps )  ->  A. x ( ph  /\  ps ) )
85, 7impbii 180 1  |-  ( A. x ( ph  /\  ps )  <->  ( A. x ph  /\  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   A.wal 1527
This theorem is referenced by:  19.26-2  1581  19.26-3an  1582  19.35  1587  19.43OLD  1593  albiim  1598  2albiim  1599  19.27  1805  19.28  1806  ax12olem2  1869  ax11eq  2132  ax11el  2133  2eu4  2226  bm1.1  2268  r19.26m  2678  unss  3349  ralunb  3356  ssin  3391  intun  3894  intpr  3895  eqrelrel  4788  relop  4834  eqoprab2b  5906  dfer2  6661  axgroth4  8454  grothprim  8456  caubnd  11842  pgapspf2  26053  dford4  27122  a12stdy2-x12  29112  a12study4  29117  a12stdy2  29127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator