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

Theorem ralimdva 2430
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 1462 . 2  |-  F/ x ph
2 ralimdva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
31, 2ralimdaa 2429 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 1434   A.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:  ralimdv  2431  f1mpt  5442  isores3  5486  caofrss  5766  caoftrn  5767  tfrlemibxssdm  5976  tfr1onlembxssdm  5992  tfrcllembxssdm  6005  tfrcl  6013  caucvgsrlemoffcau  7036  caucvgsrlemoffres  7038  indstr  8762  caucvgre  10005  rexuz3  10014  resqrexlemgt0  10044  resqrexlemglsq  10046  cau3lem  10138  rexanre  10244  rexico  10245  2clim  10278  climcn1  10285  climcn2  10286  subcn2  10288  climsqz  10311  climsqz2  10312  climcvg1nlem  10324  bezoutlemaz  10536  bezoutlembz  10537  bezoutlembi  10538
  Copyright terms: Public domain W3C validator