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

Theorem 19.26 1583
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 1549 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ph )
3 simpr 447 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43alimi 1549 . . 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 1552 . 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 1530
This theorem is referenced by:  19.26-2  1584  19.26-3an  1585  19.35  1590  19.43OLD  1596  albiim  1601  2albiim  1602  19.27  1817  19.28  1818  ax12olem2  1881  ax11eq  2145  ax11el  2146  2eu4  2239  bm1.1  2281  r19.26m  2691  unss  3362  ralunb  3369  ssin  3404  intun  3910  intpr  3911  eqrelrel  4804  relop  4850  eqoprab2b  5922  dfer2  6677  axgroth4  8470  grothprim  8472  caubnd  11858  pgapspf2  26156  dford4  27225  ax12olem2wAUX7  29433  ax7w9AUX7  29630  ax12olem2OLD7  29660  a12stdy2-x12  29734  a12study4  29739  a12stdy2  29749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator