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

Theorem 19.26 1581
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 1547 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ph )
3 simpr 449 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43alimi 1547 . . 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 1528
This theorem is referenced by:  19.26-2  1582  19.26-3an  1583  19.35  1588  19.43OLD  1594  albiim  1599  2albiim  1600  19.27  1807  19.28  1808  ax12olem2  1871  ax11eq  2134  ax11el  2135  2eu4  2228  bm1.1  2270  r19.26m  2680  unss  3351  ralunb  3358  ssin  3393  intun  3896  intpr  3897  eqrelrel  4788  relop  4834  eqoprab2b  5868  dfer2  6657  axgroth4  8450  grothprim  8452  caubnd  11837  pgapspf2  25453  dford4  26522  a12stdy2-x12  28380  a12study4  28385  a12stdy2  28395
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator