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

Theorem 19.26 1647
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 457 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21alimi 1604 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ph )
3 simpr 461 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43alimi 1604 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ps )
52, 4jca 532 . 2  |-  ( A. x ( ph  /\  ps )  ->  ( A. x ph  /\  A. x ps ) )
6 id 22 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ps ) )
76alanimi 1607 . 2  |-  ( ( A. x ph  /\  A. x ps )  ->  A. x ( ph  /\  ps ) )
85, 7impbii 188 1  |-  ( A. x ( ph  /\  ps )  <->  ( A. x ph  /\  A. x ps ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   A.wal 1367
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  19.26-2  1648  19.26-3an  1649  19.35OLD  1655  19.43OLD  1661  albiim  1665  2albiim  1666  19.27  1856  19.28  1857  ax12eq  2242  ax12el  2243  2eu4OLD  2369  bm1.1OLD  2428  r19.26m  2871  unss  3549  ralunb  3556  ssin  3591  intun  4179  intpr  4180  eqrelrel  4960  relop  5009  eqoprab2b  6163  dfer2  7121  axgroth4  9018  grothprim  9020  caubnd  12865  wl-alanbii  28417  dford4  29401  alimp-no-surprise  31156
  Copyright terms: Public domain W3C validator