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  5912  isores3  5956  caofrss  6267  caoftrn  6268  tfrlemibxssdm  6493  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  tfrcl  6530  infidc  7133  exmidomniim  7340  exmidontri2or  7461  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  indstr  9827  caucvgre  11546  rexuz3  11555  resqrexlemgt0  11585  resqrexlemglsq  11587  cau3lem  11679  rexanre  11785  rexico  11786  2clim  11866  climcn1  11873  climcn2  11874  subcn2  11876  climsqz  11900  climsqz2  11901  climcvg1nlem  11914  fprodsplitdc  12162  bezoutlemaz  12579  bezoutlembz  12580  bezoutlembi  12581  pcfac  12928  pockthg  12935  infpnlem1  12937  isgrpinv  13642  dfgrp3me  13688  issubg4m  13785  mplsubgfileminv  14720  cncnp  14960  txlm  15009  metequiv2  15226  metcnpi3  15247  rescncf  15311  cncfco  15321  suplociccreex  15354  limcresi  15396  cnplimcim  15397  cnplimclemr  15399  cnlimcim  15401  limccnpcntop  15405  limccoap  15408  2sqlem6  15855  wlkvtxiedg  16202  wlkvtxiedgg  16203  upgrwlkvtxedg  16221  uspgr2wlkeq  16222  clwwlkccatlem  16257  bj-charfunbi  16432  nninffeq  16648  tridceq  16687