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

Theorem r19.26 2532
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 108 . . . 4  |-  ( (
ph  /\  ps )  ->  ph )
21ralimi 2469 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ph )
3 simpr 109 . . . 4  |-  ( (
ph  /\  ps )  ->  ps )
43ralimi 2469 . . 3  |-  ( A. x  e.  A  ( ph  /\  ps )  ->  A. x  e.  A  ps )
52, 4jca 302 . 2  |-  ( A. x  e.  A  ( ph  /\  ps )  -> 
( A. x  e.  A  ph  /\  A. x  e.  A  ps ) )
6 pm3.2 138 . . . 4  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
76ral2imi 2471 . . 3  |-  ( A. x  e.  A  ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ( ph  /\  ps )
) )
87imp 123 . 2  |-  ( ( A. x  e.  A  ph 
/\  A. x  e.  A  ps )  ->  A. x  e.  A  ( ph  /\ 
ps ) )
95, 8impbii 125 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 103    <-> wb 104   A.wral 2390
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408
This theorem depends on definitions:  df-bi 116  df-ral 2395
This theorem is referenced by:  r19.27v  2533  r19.28v  2534  r19.26-2  2535  r19.26-3  2536  ralbiim  2540  r19.27av  2541  reu8  2849  ssrab  3141  r19.28m  3418  r19.27m  3424  2ralunsn  3691  iuneq2  3795  cnvpom  5039  funco  5121  fncnv  5147  funimaexglem  5164  fnres  5197  fnopabg  5204  mpteqb  5465  eqfnfv3  5474  caoftrn  5961  iinerm  6455  ixpeq2  6560  ixpin  6571  rexanuz  10652  recvguniq  10659  cau3lem  10778  rexanre  10884  bezoutlemmo  11540  sqrt2irr  11686  tgval2  12063  metequiv  12484  metequiv2  12485  mulcncflem  12576  bj-indind  12822
  Copyright terms: Public domain W3C validator