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  5977  isores3  6021  caofrss  6334  caoftrn  6335  tfrlemibxssdm  6598  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  tfrcl  6635  infidc  7248  exmidomniim  7482  exmidontri2or  7603  caucvgsrlemoffcau  8166  caucvgsrlemoffres  8168  indstr  10003  caucvgre  11763  rexuz3  11772  resqrexlemgt0  11802  resqrexlemglsq  11804  cau3lem  11897  rexanre  12003  rexico  12004  fiidxsupcl  12012  2clim  12086  climcn1  12093  climcn2  12094  subcn2  12096  climsqz  12120  climsqz2  12121  climcvg1nlem  12134  fprodsplitdc  12382  bezoutlemaz  12799  bezoutlembz  12800  bezoutlembi  12801  sqrtrirr  13008  pcfac  13152  pockthg  13159  infpnlem1  13161  isgrpinv  13912  dfgrp3me  13958  issubg4m  14049  mplsubgfileminv  15182  cncnp  15422  txlm  15471  metequiv2  15688  metcnpi3  15709  rescncf  15773  cncfco  15783  suplociccreex  15816  limcresi  15858  cnplimcim  15859  cnplimclemr  15861  cnlimcim  15863  limccnpcntop  15867  limccoap  15870  2sqlem6  16405  wlkvtxiedg  16752  wlkvtxiedgg  16753  upgrwlkvtxedg  16771  uspgr2wlkeq  16772  clwwlkccatlem  16807  bj-charfunbi  17003  nninffeq  17229  tridceq  17273