Theorem ralimdva 2597

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200  ∀wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  ralimdv  2598  ralimdvva  2599  f1mpt  5901  isores3  5945  caofrss  6256  caoftrn  6257  tfrlemibxssdm  6479  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  tfrcl  6516  infidc  7112  exmidomniim  7319  exmidontri2or  7439  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  indstr  9800  caucvgre  11507  rexuz3  11516  resqrexlemgt0  11546  resqrexlemglsq  11548  cau3lem  11640  rexanre  11746  rexico  11747  2clim  11827  climcn1  11834  climcn2  11835  subcn2  11837  climsqz  11861  climsqz2  11862  climcvg1nlem  11875  fprodsplitdc  12122  bezoutlemaz  12539  bezoutlembz  12540  bezoutlembi  12541  pcfac  12888  pockthg  12895  infpnlem1  12897  isgrpinv  13602  dfgrp3me  13648  issubg4m  13745  mplsubgfileminv  14679  cncnp  14919  txlm  14968  metequiv2  15185  metcnpi3  15206  rescncf  15270  cncfco  15280  suplociccreex  15313  limcresi  15355  cnplimcim  15356  cnplimclemr  15358  cnlimcim  15360  limccnpcntop  15364  limccoap  15367  2sqlem6  15814  wlkvtxiedg  16086  wlkvtxiedgg  16087  upgrwlkvtxedg  16105  uspgr2wlkeq  16106  clwwlkccatlem  16137  bj-charfunbi  16229  nninffeq  16446  tridceq  16484