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

Theorem ralrimivva 2444
 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 2443 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 102   ∈ wcel 1434  ∀wral 2349 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 1377  ax-gen 1379  ax-4 1441  ax-17 1460 This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2354 This theorem is referenced by:  swopo  4063  sosng  4433  fcof1  5448  fliftfund  5462  isoresbr  5474  isocnv  5476  f1oiso  5490  caovclg  5678  caovcomg  5681  off  5749  caofrss  5760  fmpt2co  5862  poxp  5878  f1od2  5881  eroprf  6258  dom2lem  6311  xpf1o  6375  nnwetri  6426  supmoti  6455  supsnti  6467  supisoti  6472  addlocpr  6777  mullocpr  6812  cauappcvgprlemloc  6893  cauappcvgprlemlim  6902  caucvgprlemloc  6916  caucvgprprlemloc  6944  rereceu  7106  cju  8094  exbtwnz  9326  frec2uzf1od  9477  frec2uzisod  9478  frecuzrdgrrn  9479  frec2uzrdg  9480  frecuzrdgrcl  9481  frecuzrdgsuc  9485  frecuzrdgrclt  9486  frecuzrdgg  9487  frecuzrdgsuctlem  9494  iseqoveq  9529  iseqcaopr3  9545  iseqcaopr2  9546  iseqhomo  9554  iseqdistr  9556  rsqrmo  10040  climcn2  10275  addcn2  10276  mulcn2  10278  divalglemeunn  10454  divalglemeuneg  10456  bezoutlemeu  10529  isprm6  10659  pw2dvdseu  10679
 Copyright terms: Public domain W3C validator