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

Theorem ralimi 2498
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 2496 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1481   A.wral 2417
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 1424  ax-gen 1426
This theorem depends on definitions:  df-bi 116  df-ral 2422
This theorem is referenced by:  2ralimi  2499  ral2imi  2500  r19.26  2561  r19.29  2572  rr19.3v  2827  rr19.28v  2828  reu3  2878  uniiunlem  3190  reupick2  3367  uniss2  3775  ss2iun  3836  iineq2  3838  iunss2  3866  disjss2  3917  disjeq2  3918  disjnim  3928  repizf  4052  abnexg  4375  reusv3i  4388  tfis  4505  ssrel2  4637  issref  4929  dmmptg  5044  funco  5171  fununi  5199  fun11uni  5201  funimaexglem  5214  fnmpt  5257  fun11iun  5396  mpteqb  5519  chfnrn  5539  dffo5  5577  ffvresb  5591  fmptcof  5595  dfmptg  5607  mpo2eqb  5888  ralrnmpo  5893  rexrnmpo  5894  fnmpo  6108  mpoexxg  6116  smores  6197  riinerm  6510  ixpm  6632  difinfinf  6994  cc4f  7101  cc4n  7103  cauappcvgprlemdisj  7483  caucvgsrlemasr  7622  caucvgsr  7634  suplocsr  7641  rexuz3  10794  recvguniq  10799  cau3lem  10918  caubnd2  10921  rexanre  11024  climi2  11089  climi0  11090  climcaucn  11152  ndvdssub  11663  gcdsupex  11682  gcdsupcl  11683  bezoutlemmo  11730  eltg2b  12262  neipsm  12362  lmcvg  12425  txlm  12487  metrest  12714  mulcncflem  12798  bj-indint  13300  bj-indind  13301  bj-bdfindis  13316  setindis  13336  bdsetindis  13338
  Copyright terms: Public domain W3C validator