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  5907  isores3  5951  caofrss  6262  caoftrn  6263  tfrlemibxssdm  6488  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  tfrcl  6525  infidc  7124  exmidomniim  7331  exmidontri2or  7451  caucvgsrlemoffcau  8008  caucvgsrlemoffres  8010  indstr  9817  caucvgre  11532  rexuz3  11541  resqrexlemgt0  11571  resqrexlemglsq  11573  cau3lem  11665  rexanre  11771  rexico  11772  2clim  11852  climcn1  11859  climcn2  11860  subcn2  11862  climsqz  11886  climsqz2  11887  climcvg1nlem  11900  fprodsplitdc  12147  bezoutlemaz  12564  bezoutlembz  12565  bezoutlembi  12566  pcfac  12913  pockthg  12920  infpnlem1  12922  isgrpinv  13627  dfgrp3me  13673  issubg4m  13770  mplsubgfileminv  14704  cncnp  14944  txlm  14993  metequiv2  15210  metcnpi3  15231  rescncf  15295  cncfco  15305  suplociccreex  15338  limcresi  15380  cnplimcim  15381  cnplimclemr  15383  cnlimcim  15385  limccnpcntop  15389  limccoap  15392  2sqlem6  15839  wlkvtxiedg  16142  wlkvtxiedgg  16143  upgrwlkvtxedg  16161  uspgr2wlkeq  16162  clwwlkccatlem  16195  bj-charfunbi  16342  nninffeq  16558  tridceq  16596