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

Theorem r19.26 2486
Description: Theorem 19.26 of [Margaris] p. 90 with restricted quantifiers. (Contributed by NM, 28-Jan-1997.) (Proof shortened by Andrew Salmon, 30-May-2011.)
Assertion
Ref Expression
r19.26  |-  ( A. x  e.  A  ( ph  /\  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )

Proof of Theorem r19.26
StepHypRef Expression
1 simpl 107 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21ralimi 2427 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 108 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2427 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ps )
52, 4jca 300 . 2  |-  ( A. x  e.  A  ( ph  /\  ps )  -> 
( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
6 pm3.2 137 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
76ral2imi 2428 . . 3  |-  ( A. x  e.  A  ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ( ph  /\  ps )
) )
87imp 122 . 2  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  A. x  e.  A  ( ph  /\ 
ps ) )
95, 8impbii 124 1  |-  ( A. x  e.  A  ( ph  /\  ps )  <->  ( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103   A.wral 2349
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379
This theorem depends on definitions:  df-bi 115  df-ral 2354
This theorem is referenced by:  r19.26-2  2487  r19.26-3  2488  ralbiim  2492  r19.27av  2493  reu8  2789  ssrab  3073  r19.28m  3338  r19.27m  3344  2ralunsn  3598  iuneq2  3702  cnvpom  4890  funco  4970  fncnv  4996  funimaexglem  5013  fnres  5046  fnopabg  5053  mpteqb  5293  eqfnfv3  5299  caoftrn  5767  iinerm  6244  rexanuz  10012  recvguniq  10019  cau3lem  10138  rexanre  10244  bezoutlemmo  10539  sqrt2irr  10685  bj-indind  10885
  Copyright terms: Public domain W3C validator