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

Theorem 19.26 1442
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 108 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21alimi 1416 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ph )
3 simpr 109 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43alimi 1416 . . 3  |-  ( A. x ( ph  /\  ps )  ->  A. x ps )
52, 4jca 304 . 2  |-  ( A. x ( ph  /\  ps )  ->  ( A. x ph  /\  A. x ps ) )
6 id 19 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  ps ) )
76alanimi 1420 . 2  |-  ( ( A. x ph  /\  A. x ps )  ->  A. x ( ph  /\  ps ) )
85, 7impbii 125 1  |-  ( A. x ( ph  /\  ps )  <->  ( A. x ph  /\  A. x ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104   A.wal 1314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  19.26-2  1443  19.26-3an  1444  albiim  1448  2albiim  1449  hband  1450  hban  1511  19.27h  1524  19.27  1525  19.28h  1526  19.28  1527  nford  1531  nfand  1532  equsexd  1692  equveli  1717  sbanv  1845  2eu4  2070  bm1.1  2102  r19.26m  2540  unss  3220  ralunb  3227  ssin  3268  intun  3772  intpr  3773  eqrelrel  4610  relop  4659  eqoprab2b  5797  dfer2  6398
  Copyright terms: Public domain W3C validator