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

Theorem ralimdva 2387
 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
Assertion
Ref Expression
ralimdva
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem ralimdva
StepHypRef Expression
1 nfv 1421 . 2
2 ralimdva.1 . 2
31, 2ralimdaa 2386 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:  ralimdv  2388  f1mpt  5410  isores3  5455  caofrss  5735  caoftrn  5736  tfrlemibxssdm  5941  rdgon  5973  caucvgsrlemoffcau  6882  caucvgsrlemoffres  6884  indstr  8536  caucvgre  9580  rexuz3  9588  resqrexlemgt0  9618  resqrexlemglsq  9620  cau3lem  9710  2clim  9822  climcn1  9829  climcn2  9830  subcn2  9832  climsqz  9855  climsqz2  9856  climcvg1nlem  9868
 Copyright terms: Public domain W3C validator