Theorem ralimdva 2611

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 2610	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2205  ∀wral 2522

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 2527

This theorem is referenced by:  ralimdv  2612  ralimdvva  2613  f1mpt  5950  isores3  5994  caofrss  6307  caoftrn  6308  tfrlemibxssdm  6571  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  tfrcl  6608  infidc  7214  exmidomniim  7445  exmidontri2or  7566  caucvgsrlemoffcau  8129  caucvgsrlemoffres  8131  indstr  9943  caucvgre  11691  rexuz3  11700  resqrexlemgt0  11730  resqrexlemglsq  11732  cau3lem  11824  rexanre  11930  rexico  11931  2clim  12011  climcn1  12018  climcn2  12019  subcn2  12021  climsqz  12045  climsqz2  12046  climcvg1nlem  12059  fprodsplitdc  12307  bezoutlemaz  12724  bezoutlembz  12725  bezoutlembi  12726  pcfac  13073  pockthg  13080  infpnlem1  13082  isgrpinv  13809  dfgrp3me  13855  issubg4m  13946  mplsubgfileminv  14981  cncnp  15221  txlm  15270  metequiv2  15487  metcnpi3  15508  rescncf  15572  cncfco  15582  suplociccreex  15615  limcresi  15657  cnplimcim  15658  cnplimclemr  15660  cnlimcim  15662  limccnpcntop  15666  limccoap  15669  2sqlem6  16119  wlkvtxiedg  16466  wlkvtxiedgg  16467  upgrwlkvtxedg  16485  uspgr2wlkeq  16486  clwwlkccatlem  16521  bj-charfunbi  16707  nninffeq  16924  tridceq  16967