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

Theorem 19.26 1725
Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 147. (Contributed by NM, 12-Mar-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 458 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21alimi 1680 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ph )
3 simpr 462 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43alimi 1680 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ps )
52, 4jca 534 . 2  |-  ( A. x ( ph  /\  ps )  ->  ( A. x ph  /\  A. x ps ) )
6 id 23 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ps ) )
76alanimi 1684 . 2  |-  ( ( A. x ph  /\  A. x ps )  ->  A. x ( ph  /\  ps ) )
85, 7impbii 190 1  |-  ( A. x ( ph  /\  ps )  <->  ( A. x ph  /\  A. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370   A.wal 1435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678
This theorem depends on definitions:  df-bi 188  df-an 372
This theorem is referenced by:  19.26-2  1726  19.26-3an  1727  19.43OLD  1738  albiim  1743  2albiim  1744  19.27v  1813  19.28v  1814  19.27  1979  19.28  1980  bm1.1OLD  2406  r19.26m  2958  unss  3640  ralunb  3647  ssin  3684  intun  4285  intpr  4286  eqrelrel  4951  relop  5000  eqoprab2b  6359  dfer2  7368  axgroth4  9257  grothprim  9259  trclfvcotr  13061  caubnd  13409  bj-gl4lem  31169  bj-gl4  31170  wl-alanbii  31811  ax12eq  32430  ax12el  32431  dford4  35803  alimp-no-surprise  39793
  Copyright terms: Public domain W3C validator