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

Theorem ralrimivw 2447
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
ralrimivw.1 (𝜑𝜓)
Assertion
Ref Expression
ralrimivw (𝜑 → ∀𝑥𝐴 𝜓)
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem ralrimivw
StepHypRef Expression
1 ralrimivw.1 . . 3 (𝜑𝜓)
21a1d 22 . 2 (𝜑 → (𝑥𝐴𝜓))
32ralrimiv 2445 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1438  wral 2359
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 1381  ax-gen 1383  ax-4 1445  ax-17 1464
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364
This theorem is referenced by:  exse  4154  sosng  4499  dmxpm  4644  exse2  4793  funco  5040  acexmidlemph  5627  mpt2eq12  5691  xpexgALT  5886  mpt2exg  5960  rdgtfr  6121  rdgruledefgg  6122  rdgivallem  6128  frecabex  6145  frectfr  6147  omfnex  6192  oeiv  6199  uniqs  6330  sbthlemi5  6649  sbthlemi6  6650  updjud  6752  exmidfodomrlemim  6806  genpdisj  7061  ltexprlemloc  7145  recexprlemloc  7169  cauappcvgprlemrnd  7188  cauappcvgprlemdisj  7189  caucvgprlemrnd  7211  caucvgprlemdisj  7212  caucvgprprlemrnd  7239  caucvgprprlemdisj  7240  recan  10507  climconst  10642  sumeq2ad  10722  dvdsext  10949
  Copyright terms: Public domain W3C validator