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

Theorem ralimi 2540
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 2538 1 (∀𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2148  wral 2455
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449
This theorem depends on definitions:  df-bi 117  df-ral 2460
This theorem is referenced by:  2ralimi  2541  ral2imi  2542  r19.26  2603  r19.29  2614  rr19.3v  2876  rr19.28v  2877  reu3  2927  uniiunlem  3244  reupick2  3421  uniss2  3838  ss2iun  3899  iineq2  3901  iunss2  3929  disjss2  3980  disjeq2  3981  disjnim  3991  repizf  4116  abnexg  4442  reusv3i  4455  tfis  4578  ssrel2  4712  issref  5006  dmmptg  5121  funco  5251  fununi  5279  fun11uni  5281  funimaexglem  5294  fnmpt  5337  fun11iun  5477  mpteqb  5601  chfnrn  5622  dffo5  5660  ffvresb  5674  fmptcof  5678  dfmptg  5690  mpo2eqb  5977  ralrnmpo  5982  rexrnmpo  5983  fnmpo  6196  mpoexxg  6204  smores  6286  riinerm  6601  ixpm  6723  difinfinf  7093  nninfwlpoimlemginf  7167  exmidontriimlem1  7213  onntri13  7230  onntri24  7234  cc4f  7246  cc4n  7248  cauappcvgprlemdisj  7628  caucvgsrlemasr  7767  caucvgsr  7779  suplocsr  7786  rexuz3  10970  recvguniq  10975  cau3lem  11094  caubnd2  11097  rexanre  11200  climi2  11267  climi0  11268  climcaucn  11330  ndvdssub  11905  gcdsupex  11928  gcdsupcl  11929  bezoutlemmo  11977  mgmidmo  12670  eltg2b  13187  neipsm  13287  lmcvg  13350  txlm  13412  metrest  13639  mulcncflem  13723  bj-charfunbi  14185  bj-indint  14305  bj-indind  14306  bj-bdfindis  14321  setindis  14341  bdsetindis  14343
  Copyright terms: Public domain W3C validator