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

Theorem ralimdva 2441
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
ralimdva.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ralimdva  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem ralimdva
StepHypRef Expression
1 nfv 1466 . 2  |-  F/ x ph
2 ralimdva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
31, 2ralimdaa 2440 1  |-  ( ph  ->  ( A. x  e.  A  ps  ->  A. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    e. wcel 1438   A.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:  ralimdv  2442  f1mpt  5542  isores3  5586  caofrss  5871  caoftrn  5872  tfrlemibxssdm  6084  tfr1onlembxssdm  6100  tfrcllembxssdm  6113  tfrcl  6121  exmidomniim  6787  caucvgsrlemoffcau  7333  caucvgsrlemoffres  7335  indstr  9071  caucvgre  10402  rexuz3  10411  resqrexlemgt0  10441  resqrexlemglsq  10443  cau3lem  10535  rexanre  10641  rexico  10642  2clim  10676  climcn1  10684  climcn2  10685  subcn2  10687  climsqz  10710  climsqz2  10711  climcvg1nlem  10725  bezoutlemaz  11257  bezoutlembz  11258  bezoutlembi  11259  rescncf  11520  cncfco  11530
  Copyright terms: Public domain W3C validator