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

Theorem ralimi 2378
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 2376 1
Colors of variables: wff set class
Syntax hints:   wi 4   wcel 1390  wral 2300
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335
This theorem depends on definitions:  df-bi 110  df-ral 2305
This theorem is referenced by:  ral2imi  2379  r19.26  2435  r19.29  2444  rr19.3v  2676  rr19.28v  2677  reu3  2725  uniiunlem  3022  reupick2  3217  uniss2  3602  ss2iun  3663  iineq2  3665  iunss2  3693  disjss2  3739  disjeq2  3740  repizf  3864  reusv3i  4157  tfis  4249  ssrel2  4373  issref  4650  dmmptg  4761  funco  4883  fununi  4910  fun11uni  4912  funimaexglem  4925  fnmpt  4968  fun11iun  5090  mpteqb  5204  chfnrn  5221  dffo5  5259  ffvresb  5271  fmptcof  5274  dfmptg  5285  mpt22eqb  5552  ralrnmpt2  5557  rexrnmpt2  5558  fnmpt2  5770  mpt2exxg  5775  smores  5848  riinerm  6115  cauappcvgprlemdisj  6623  bj-indint  9390  bj-indind  9391  bj-bdfindis  9407  setindis  9427  bdsetindis  9429
  Copyright terms: Public domain W3C validator