Theorem ralimdva 2599

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

Step	Hyp	Ref	Expression
1		nfv 1576	. 2 ⊢ Ⅎ𝑥𝜑
2		ralimdva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	1, 2	ralimdaa 2598	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202  ∀wral 2510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  ralimdv  2600  ralimdvva  2601  f1mpt  5911  isores3  5955  caofrss  6266  caoftrn  6267  tfrlemibxssdm  6492  tfr1onlembxssdm  6508  tfrcllembxssdm  6521  tfrcl  6529  infidc  7132  exmidomniim  7339  exmidontri2or  7460  caucvgsrlemoffcau  8017  caucvgsrlemoffres  8019  indstr  9826  caucvgre  11541  rexuz3  11550  resqrexlemgt0  11580  resqrexlemglsq  11582  cau3lem  11674  rexanre  11780  rexico  11781  2clim  11861  climcn1  11868  climcn2  11869  subcn2  11871  climsqz  11895  climsqz2  11896  climcvg1nlem  11909  fprodsplitdc  12156  bezoutlemaz  12573  bezoutlembz  12574  bezoutlembi  12575  pcfac  12922  pockthg  12929  infpnlem1  12931  isgrpinv  13636  dfgrp3me  13682  issubg4m  13779  mplsubgfileminv  14713  cncnp  14953  txlm  15002  metequiv2  15219  metcnpi3  15240  rescncf  15304  cncfco  15314  suplociccreex  15347  limcresi  15389  cnplimcim  15390  cnplimclemr  15392  cnlimcim  15394  limccnpcntop  15398  limccoap  15401  2sqlem6  15848  wlkvtxiedg  16195  wlkvtxiedgg  16196  upgrwlkvtxedg  16214  uspgr2wlkeq  16215  clwwlkccatlem  16250  bj-charfunbi  16406  nninffeq  16622  tridceq  16660