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

Theorem 19.26 1604
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 1569 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ph )
3 simpr 449 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43alimi 1569 . . 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 1572 . 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 1550
This theorem is referenced by:  19.26-2  1605  19.26-3an  1606  19.35  1611  19.43OLD  1617  albiim  1622  2albiim  1623  19.27  1842  19.28  1843  ax11eq  2271  ax11el  2272  2eu4  2365  bm1.1  2422  r19.26m  2842  unss  3522  ralunb  3529  ssin  3564  intun  4083  intpr  4084  eqrelrel  4978  relop  5024  eqoprab2b  6133  dfer2  6907  axgroth4  8708  grothprim  8710  caubnd  12163  dford4  27101  ax12olem2wAUX7  29457  ax7w9AUX7  29661  ax7w10AUX7  29663  ax12olem2OLD7  29707
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator