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

Theorem ralimdva 2500
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 1509 . 2 𝑥𝜑
2 ralimdva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2ralimdaa 2499 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1481  wral 2417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422
This theorem is referenced by:  ralimdv  2501  ralimdvva  2502  f1mpt  5676  isores3  5720  caofrss  6010  caoftrn  6011  tfrlemibxssdm  6228  tfr1onlembxssdm  6244  tfrcllembxssdm  6257  tfrcl  6265  exmidomniim  7017  caucvgsrlemoffcau  7626  caucvgsrlemoffres  7628  indstr  9411  caucvgre  10781  rexuz3  10790  resqrexlemgt0  10820  resqrexlemglsq  10822  cau3lem  10914  rexanre  11020  rexico  11021  2clim  11098  climcn1  11105  climcn2  11106  subcn2  11108  climsqz  11132  climsqz2  11133  climcvg1nlem  11146  bezoutlemaz  11718  bezoutlembz  11719  bezoutlembi  11720  cncnp  12429  txlm  12478  metequiv2  12695  metcnpi3  12716  rescncf  12767  cncfco  12777  suplociccreex  12801  limcresi  12834  cnplimcim  12835  cnplimclemr  12837  cnlimcim  12839  limccnpcntop  12843  limccoap  12846  nninffeq  13374
  Copyright terms: Public domain W3C validator