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

Theorem ralrimivva 2514
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.)
Hypothesis
Ref Expression
ralrimivva.1 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝜓)
Assertion
Ref Expression
ralrimivva (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Distinct variable groups:   𝜑,𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem ralrimivva
StepHypRef Expression
1 ralrimivva.1 . . 3 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝜓)
21ex 114 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜓))
32ralrimivv 2513 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1480  wral 2416
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421
This theorem is referenced by:  swopo  4228  sosng  4612  fcof1  5684  fliftfund  5698  isoresbr  5710  isocnv  5712  f1oiso  5727  caovclg  5923  caovcomg  5926  off  5994  caofrss  6006  oprssdmm  6069  dmmpog  6107  fnmpoovd  6112  fmpoco  6113  poxp  6129  f1od2  6132  eroprf  6522  dom2lem  6666  xpf1o  6738  fidifsnid  6765  nnwetri  6804  undiffi  6813  fidcenumlemim  6840  supmoti  6880  supsnti  6892  supisoti  6897  difinfsnlem  6984  cc2lem  7086  addlocpr  7356  mullocpr  7391  cauappcvgprlemloc  7472  cauappcvgprlemlim  7481  caucvgprlemloc  7495  caucvgprprlemloc  7523  suplocexprlemloc  7541  suplocsrlemb  7626  rereceu  7709  axpre-suploclemres  7721  ltordlem  8256  cju  8731  exbtwnz  10040  frec2uzf1od  10191  frec2uzisod  10192  frecuzrdgrrn  10193  frec2uzrdg  10194  frecuzrdgrcl  10195  frecuzrdgsuc  10199  frecuzrdgrclt  10200  frecuzrdgg  10201  frecuzrdgsuctlem  10208  seqvalcd  10244  seqovcd  10248  seq3caopr3  10266  seq3caopr2  10267  iseqf1olemqf1o  10278  seq3homo  10295  seq3distr  10298  fimaxq  10585  zfz1isolem1  10595  rsqrmo  10811  climcn2  11090  addcn2  11091  mulcn2  11093  fsum2dlemstep  11215  fisumcom2  11219  cvgratnn  11312  divalglemeunn  11629  divalglemeuneg  11631  bezoutlemeu  11706  isprm6  11836  pw2dvdseu  11857  crth  11911  ennnfonelemim  11948  tgclb  12248  txbas  12441  txcnp  12454  txcnmpt  12456  cnmpt21  12474  txswaphmeo  12504  isxmetd  12530  isxmet2d  12531  xmettpos  12553  blfvalps  12568  xmetresbl  12623  metss2  12681  comet  12682  bdmet  12685  bdmopn  12687  xmetxp  12690  qtopbasss  12704  elcncf1di  12749  cncffvrn  12752  mulc1cncf  12759  cncfco  12761  dedekindeulemloc  12780  dedekindeu  12784  dedekindicclemloc  12789  dedekindicclemicc  12793  ivthinclemloc  12802  sssneq  13281  exmidsbthrlem  13303  cvgcmp2n  13314  trirec0  13323  apdiff  13327
  Copyright terms: Public domain W3C validator