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

Theorem 19.26 1600
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 444 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21alimi 1565 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ph )
3 simpr 448 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43alimi 1565 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ps )
52, 4jca 519 . 2  |-  ( A. x ( ph  /\  ps )  ->  ( A. x ph  /\  A. x ps ) )
6 id 20 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ps ) )
76alanimi 1568 . 2  |-  ( ( A. x ph  /\  A. x ps )  ->  A. x ( ph  /\  ps ) )
85, 7impbii 181 1  |-  ( A. x ( ph  /\  ps )  <->  ( A. x ph  /\  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   A.wal 1546
This theorem is referenced by:  19.26-2  1601  19.26-3an  1602  19.35  1607  19.43OLD  1613  albiim  1618  2albiim  1619  19.27  1837  19.28  1838  ax11eq  2243  ax11el  2244  2eu4  2337  bm1.1  2389  r19.26m  2801  unss  3481  ralunb  3488  ssin  3523  intun  4042  intpr  4043  eqrelrel  4936  relop  4982  eqoprab2b  6091  dfer2  6865  axgroth4  8663  grothprim  8665  caubnd  12117  dford4  26990  ax12olem2wAUX7  29162  ax7w9AUX7  29360  ax12olem2OLD7  29390
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator