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

Theorem ralrimivva 2451
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 113 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜓))
32ralrimivv 2450 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  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  ax-4 1443  ax-17 1462
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-ral 2360
This theorem is referenced by:  swopo  4107  sosng  4479  fcof1  5523  fliftfund  5537  isoresbr  5549  isocnv  5551  f1oiso  5566  caovclg  5754  caovcomg  5757  off  5825  caofrss  5836  fmpt2co  5938  poxp  5954  f1od2  5957  eroprf  6337  dom2lem  6441  xpf1o  6512  fidifsnid  6539  nnwetri  6578  undiffi  6587  supmoti  6632  supsnti  6644  supisoti  6649  addlocpr  7039  mullocpr  7074  cauappcvgprlemloc  7155  cauappcvgprlemlim  7164  caucvgprlemloc  7178  caucvgprprlemloc  7206  rereceu  7368  cju  8356  exbtwnz  9590  frec2uzf1od  9741  frec2uzisod  9742  frecuzrdgrrn  9743  frec2uzrdg  9744  frecuzrdgrcl  9745  frecuzrdgsuc  9749  frecuzrdgrclt  9750  frecuzrdgg  9751  frecuzrdgsuctlem  9758  iseqoveq  9798  iseqcaopr3  9814  iseqcaopr2  9815  iseqf1olemqf1o  9826  iseqhomo  9844  iseqdistr  9846  fimaxq  10131  zfz1isolem1  10141  rsqrmo  10355  climcn2  10590  addcn2  10591  mulcn2  10593  divalglemeunn  10796  divalglemeuneg  10798  bezoutlemeu  10871  isprm6  11001  pw2dvdseu  11021  crth  11075  exmidsbthrlem  11350
  Copyright terms: Public domain W3C validator