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

Theorem ralimi 2438
Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralimi.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ralimi  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )

Proof of Theorem ralimi
StepHypRef Expression
1 ralimi.1 . . 3  |-  ( ph  ->  ps )
21a1i 9 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32ralimia 2436 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1438   A.wral 2359
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 1381  ax-gen 1383
This theorem depends on definitions:  df-bi 115  df-ral 2364
This theorem is referenced by:  ral2imi  2439  r19.26  2497  r19.29  2506  rr19.3v  2753  rr19.28v  2754  reu3  2803  uniiunlem  3107  reupick2  3283  uniss2  3679  ss2iun  3740  iineq2  3742  iunss2  3770  disjss2  3817  disjeq2  3818  disjnim  3828  repizf  3947  reusv3i  4272  tfis  4388  ssrel2  4516  issref  4801  dmmptg  4915  funco  5040  fununi  5068  fun11uni  5070  funimaexglem  5083  fnmpt  5126  fun11iun  5258  mpteqb  5377  chfnrn  5394  dffo5  5432  ffvresb  5445  fmptcof  5449  dfmptg  5460  mpt22eqb  5736  ralrnmpt2  5741  rexrnmpt2  5742  fnmpt2  5954  mpt2exxg  5959  smores  6039  riinerm  6345  cauappcvgprlemdisj  7189  caucvgsrlemasr  7314  caucvgsr  7326  rexuz3  10388  recvguniq  10393  cau3lem  10512  caubnd2  10515  rexanre  10618  climi2  10640  climi0  10641  climcaucn  10704  ndvdssub  11023  gcdsupex  11042  gcdsupcl  11043  bezoutlemmo  11088  bj-indint  11483  bj-indind  11484  bj-bdfindis  11499  setindis  11519  bdsetindis  11521
  Copyright terms: Public domain W3C validator