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

Theorem ralimdva 2458
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 1476 . 2 𝑥𝜑
2 ralimdva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2ralimdaa 2457 1 (𝜑 → (∀𝑥𝐴 𝜓 → ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1448  wral 2375
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474
This theorem depends on definitions:  df-bi 116  df-nf 1405  df-ral 2380
This theorem is referenced by:  ralimdv  2459  ralimdvva  2460  f1mpt  5604  isores3  5648  caofrss  5937  caoftrn  5938  tfrlemibxssdm  6154  tfr1onlembxssdm  6170  tfrcllembxssdm  6183  tfrcl  6191  exmidomniim  6925  caucvgsrlemoffcau  7493  caucvgsrlemoffres  7495  indstr  9238  caucvgre  10593  rexuz3  10602  resqrexlemgt0  10632  resqrexlemglsq  10634  cau3lem  10726  rexanre  10832  rexico  10833  2clim  10909  climcn1  10916  climcn2  10917  subcn2  10919  climsqz  10943  climsqz2  10944  climcvg1nlem  10957  bezoutlemaz  11484  bezoutlembz  11485  bezoutlembi  11486  cncnp  12180  txlm  12229  metequiv2  12424  metcnpi3  12441  rescncf  12481  cncfco  12491  limcresi  12515  cnplimcim  12516  cnlimcim  12517  limccnpcntop  12520  nninffeq  12800
  Copyright terms: Public domain W3C validator