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

Theorem ralimi 2434
Description: Inference quantifying both antecedent and consequent, with strong hypothesis. (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralimi.1 (𝜑𝜓)
Assertion
Ref Expression
ralimi (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)

Proof of Theorem ralimi
StepHypRef Expression
1 ralimi.1 . . 3 (𝜑𝜓)
21a1i 9 . 2 (𝑥𝐴 → (𝜑𝜓))
32ralimia 2432 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1436  wral 2355
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 1379  ax-gen 1381
This theorem depends on definitions:  df-bi 115  df-ral 2360
This theorem is referenced by:  ral2imi  2435  r19.26  2493  r19.29  2502  rr19.3v  2746  rr19.28v  2747  reu3  2796  uniiunlem  3098  reupick2  3274  uniss2  3669  ss2iun  3730  iineq2  3732  iunss2  3760  disjss2  3806  disjeq2  3807  repizf  3932  reusv3i  4257  tfis  4373  ssrel2  4498  issref  4783  dmmptg  4896  funco  5021  fununi  5049  fun11uni  5051  funimaexglem  5064  fnmpt  5107  fun11iun  5239  mpteqb  5358  chfnrn  5375  dffo5  5413  ffvresb  5426  fmptcof  5430  dfmptg  5441  mpt22eqb  5713  ralrnmpt2  5718  rexrnmpt2  5719  fnmpt2  5931  mpt2exxg  5936  smores  6013  riinerm  6319  cauappcvgprlemdisj  7157  caucvgsrlemasr  7282  caucvgsr  7294  rexuz3  10322  recvguniq  10327  cau3lem  10446  caubnd2  10449  rexanre  10552  climi2  10574  climi0  10575  climcaucn  10635  ndvdssub  10836  gcdsupex  10855  gcdsupcl  10856  bezoutlemmo  10901  bj-indint  11295  bj-indind  11296  bj-bdfindis  11311  setindis  11331  bdsetindis  11333
  Copyright terms: Public domain W3C validator