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

Theorem ralrimiva 2370
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)
Hypothesis
Ref Expression
ralrimiva.1 ((φ x A) → ψ)
Assertion
Ref Expression
ralrimiva (φx A ψ)
Distinct variable group:   φ,x
Allowed substitution hints:   ψ(x)   A(x)

Proof of Theorem ralrimiva
StepHypRef Expression
1 ralrimiva.1 . . 3 ((φ x A) → ψ)
21ex 108 . 2 (φ → (x Aψ))
32ralrimiv 2369 1 (φx A ψ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1374  wral 2284
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 1316  ax-gen 1318  ax-4 1381  ax-17 1400
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-ral 2289
This theorem is referenced by:  ralrimivvva  2380  rgen2  2383  rgen3  2384  nrexdv  2390  r19.29_2a  2434  rabbidva  2526  ssrabdv  2996  ss2rabdv  2998  iuneq2dv  3652  disjeq2dv  3724  mpteq12dva  3812  triun  3841  issod  4030  peano2  4245  fun11iun  5072  fniinfv  5156  eqfnfv  5190  eqfnfvd  5193  dff3im  5237  dffo4  5240  foco2  5243  fmptd  5247  ffnfv  5248  fmpt2d  5252  ffvresb  5253  fconst2g  5301  fconstfvm  5304  resfunexg  5307  eufnfv  5314  fniunfv  5326  fcofo  5349  fliftel  5358  fliftfun  5361  fliftfuns  5363  riota5f  5416  grprinvlem  5618  grprinvd  5619  f1ocnvd  5625  suppssov1  5632  offval2  5649  ofrfval2  5650  offveqb  5653  caofref  5655  caofinvl  5656  opabex3d  5671  tfrlem1  5845  tfrlemisucaccv  5860  tfrlemiubacc  5865  omcl  5956  oeicl  5957  qliftfuns  6101  genprndl  6376  genprndu  6377  nqprloc  6400  ltexprlemrnd  6442  ltexprlemdisj  6443  recexprlemrnd  6463  recexprlemdisj  6464  negeu  6789
  Copyright terms: Public domain W3C validator