ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  19.26 Unicode version

Theorem 19.26 1386
Description: Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 119. (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 106 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21alimi 1360 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ph )
3 simpr 107 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43alimi 1360 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ps )
52, 4jca 294 . 2  |-  ( A. x ( ph  /\  ps )  ->  ( A. x ph  /\  A. x ps ) )
6 id 19 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ps ) )
76alanimi 1364 . 2  |-  ( ( A. x ph  /\  A. x ps )  ->  A. x ( ph  /\  ps ) )
85, 7impbii 121 1  |-  ( A. x ( ph  /\  ps )  <->  ( A. x ph  /\  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 101    <-> wb 102   A.wal 1257
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  19.26-2  1387  19.26-3an  1388  albiim  1392  2albiim  1393  hband  1394  hban  1455  19.27h  1468  19.27  1469  19.28h  1470  19.28  1471  nford  1475  nfand  1476  equsexd  1633  equveli  1658  sbanv  1785  2eu4  2009  bm1.1  2041  r19.26m  2461  unss  3145  ralunb  3152  ssin  3187  intun  3674  intpr  3675  eqrelrel  4469  relop  4514  eqoprab2b  5591  dfer2  6138
  Copyright terms: Public domain W3C validator