Theorem ralimdva 2600

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 1577	. 2 ⊢ Ⅎ𝑥𝜑
2		ralimdva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	1, 2	ralimdaa 2599	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516

This theorem is referenced by:  ralimdv  2601  ralimdvva  2602  f1mpt  5922  isores3  5966  caofrss  6276  caoftrn  6277  tfrlemibxssdm  6536  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  tfrcl  6573  infidc  7176  exmidomniim  7383  exmidontri2or  7504  caucvgsrlemoffcau  8061  caucvgsrlemoffres  8063  indstr  9871  caucvgre  11604  rexuz3  11613  resqrexlemgt0  11643  resqrexlemglsq  11645  cau3lem  11737  rexanre  11843  rexico  11844  2clim  11924  climcn1  11931  climcn2  11932  subcn2  11934  climsqz  11958  climsqz2  11959  climcvg1nlem  11972  fprodsplitdc  12220  bezoutlemaz  12637  bezoutlembz  12638  bezoutlembi  12639  pcfac  12986  pockthg  12993  infpnlem1  12995  isgrpinv  13700  dfgrp3me  13746  issubg4m  13843  mplsubgfileminv  14784  cncnp  15024  txlm  15073  metequiv2  15290  metcnpi3  15311  rescncf  15375  cncfco  15385  suplociccreex  15418  limcresi  15460  cnplimcim  15461  cnplimclemr  15463  cnlimcim  15465  limccnpcntop  15469  limccoap  15472  2sqlem6  15922  wlkvtxiedg  16269  wlkvtxiedgg  16270  upgrwlkvtxedg  16288  uspgr2wlkeq  16289  clwwlkccatlem  16324  bj-charfunbi  16510  nninffeq  16729  tridceq  16772