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

Theorem ralimi 2427
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 2425 1  |-  ( A. x  e.  A  ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   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:  ral2imi  2428  r19.26  2486  r19.29  2495  rr19.3v  2734  rr19.28v  2735  reu3  2783  uniiunlem  3083  reupick2  3257  uniss2  3640  ss2iun  3701  iineq2  3703  iunss2  3731  disjss2  3777  disjeq2  3778  repizf  3902  reusv3i  4217  tfis  4332  ssrel2  4456  issref  4737  dmmptg  4848  funco  4970  fununi  4998  fun11uni  5000  funimaexglem  5013  fnmpt  5056  fun11iun  5178  mpteqb  5293  chfnrn  5310  dffo5  5348  ffvresb  5360  fmptcof  5363  dfmptg  5374  mpt22eqb  5641  ralrnmpt2  5646  rexrnmpt2  5647  fnmpt2  5859  mpt2exxg  5864  smores  5941  riinerm  6245  cauappcvgprlemdisj  6903  caucvgsrlemasr  7028  caucvgsr  7040  rexuz3  10014  recvguniq  10019  cau3lem  10138  caubnd2  10141  rexanre  10244  climi2  10265  climi0  10266  climcaucn  10326  ndvdssub  10474  gcdsupex  10493  gcdsupcl  10494  bezoutlemmo  10539  bj-indint  10884  bj-indind  10885  bj-bdfindis  10900  setindis  10920  bdsetindis  10922
  Copyright terms: Public domain W3C validator