Theorem ralimdva 2617

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  ralimdv  2618  ralimdvva  2619  f1mpt  5980  isores3  6024  caofrss  6338  caoftrn  6339  tfrlemibxssdm  6602  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  tfrcl  6639  infidc  7252  exmidomniim  7487  exmidontri2or  7608  caucvgsrlemoffcau  8171  caucvgsrlemoffres  8173  indstr  10009  caucvgre  11769  rexuz3  11778  resqrexlemgt0  11808  resqrexlemglsq  11810  cau3lem  11903  rexanre  12009  rexico  12010  fiidxsupcl  12018  2clim  12092  climcn1  12099  climcn2  12100  subcn2  12102  climsqz  12126  climsqz2  12127  climcvg1nlem  12140  fprodsplitdc  12388  bezoutlemaz  12805  bezoutlembz  12806  bezoutlembi  12807  sqrtrirr  13014  pcfac  13158  pockthg  13165  infpnlem1  13167  isgrpinv  13918  dfgrp3me  13964  issubg4m  14055  mplsubgfileminv  15216  cncnp  15456  txlm  15505  metequiv2  15722  metcnpi3  15743  rescncf  15807  cncfco  15817  suplociccreex  15850  limcresi  15892  cnplimcim  15893  cnplimclemr  15895  cnlimcim  15897  limccnpcntop  15901  limccoap  15904  2sqlem6  16444  wlkvtxiedg  16791  wlkvtxiedgg  16792  upgrwlkvtxedg  16810  uspgr2wlkeq  16811  clwwlkccatlem  16846  bj-charfunbi  17042  nninffeq  17269  tridceq  17313