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  2105  ax11el  2106  2eu4  2196  bm1.1  2238  r19.26m  2640  unss  3259  ralunb  3264  ssin  3298  intun  3792  intpr  3793  eqrelrel  4695  relop  4741  eqoprab2b  5758  dfer2  6547  axgroth4  8334  grothprim  8336  caubnd  11719  pgapspf2  25219  dford4  26288  a12stdy2-x12  27801  a12study4  27806  a12stdy2  27816
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