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

Theorem ralrimivva 2401
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 108 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜓))
32ralrimivv 2400 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97  wcel 1393  wral 2306
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 1336  ax-gen 1338  ax-4 1400  ax-17 1419
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311
This theorem is referenced by:  swopo  4043  sosng  4413  fcof1  5423  fliftfund  5437  isoresbr  5449  isocnv  5451  f1oiso  5465  caovclg  5653  caovcomg  5656  off  5724  caofrss  5735  fmpt2co  5837  poxp  5853  eroprf  6199  dom2lem  6252  nnwetri  6354  addlocpr  6632  mullocpr  6667  cauappcvgprlemloc  6748  cauappcvgprlemlim  6757  caucvgprlemloc  6771  caucvgprprlemloc  6799  rereceu  6961  cju  7911  qbtwnz  9104  frec2uzf1od  9166  frec2uzisod  9167  frecuzrdgrrn  9168  iseqcaopr3  9214  iseqcaopr2  9215  iseqhomo  9222  iseqdistr  9223  rsqrmo  9599  climcn2  9804  addcn2  9805  mulcn2  9807
  Copyright terms: Public domain W3C validator