Theorem ralimdv 3178

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.20 of [Margaris] p. 90 (alim 1807). (Contributed by NM, 8-Oct-2003.)

Hypothesis

Ref	Expression
ralimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
ralimdv	⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralimdv

Step	Hyp	Ref	Expression
1		ralimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	adantr 483	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 → 𝜒))
3	2	ralimdva 3177	1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2110  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3143

This theorem is referenced by:  ss2ralv  4034  poss  5470  sess1  5517  sess2  5518  riinint  5833  iinpreima  6831  dffo4  6863  dffo5  6864  isoini2  7086  tfindsg  7569  el2mpocsbcl  7774  iiner  8363  xpf1o  8673  dffi3  8889  brwdom3  9040  xpwdomg  9043  bndrank  9264  cfub  9665  cff1  9674  cfflb  9675  cfslb2n  9684  cofsmo  9685  cfcoflem  9688  pwcfsdom  9999  fpwwe2lem13  10058  inawinalem  10105  grupr  10213  fsequb  13337  cau3lem  14708  caubnd2  14711  caubnd  14712  rlim2lt  14848  rlim3  14849  climshftlem  14925  climcau  15021  caucvgb  15030  serf0  15031  modfsummods  15142  cvgcmp  15165  mreriincl  16863  acsfn1c  16927  islss4  19728  riinopn  21510  fiinbas  21554  baspartn  21556  isclo2  21690  lmcls  21904  lmcnp  21906  isnrm3  21961  1stcelcls  22063  llyss  22081  nllyss  22082  ptpjpre1  22173  txlly  22238  txnlly  22239  tx1stc  22252  xkococnlem  22261  fbunfip  22471  filssufilg  22513  cnpflf2  22602  fcfnei  22637  isucn2  22882  rescncf  23499  lebnum  23562  cfilss  23867  fgcfil  23868  iscau4  23876  cmetcaulem  23885  caussi  23894  ovolunlem1  24092  ulmclm  24969  ulmcaulem  24976  ulmcau  24977  ulmss  24979  rlimcnp  25537  cxploglim  25549  2sqreunnlem2  26025  pntlemp  26180  axcontlem4  26747  ewlkle  27381  uspgr2wlkeq  27421  umgrwlknloop  27424  wlkiswwlksupgr2  27649  3cyclfrgrrn2  28060  nmlnoubi  28567  lnon0  28569  disjpreima  30328  resspos  30641  resstos  30642  submarchi  30810  prmidl2  30953  crefss  31108  iccllysconn  32492  cvmlift2lem1  32544  dmopab3rexdif  32647  ss2mcls  32810  mclsax  32811  nosupno  33198  nosupres  33202  sssslt2  33256  isinf2  34680  poimirlem25  34911  poimirlem27  34913  upixp  34998  caushft  35030  sstotbnd3  35048  totbndss  35049  unichnidl  35303  ispridl2  35310  elrfirn2  39286  mzpsubst  39338  eluzrabdioph  39396  neik0pk1imk0  40390  mnuop3d  40600  limsupub  41978  limsupre3lem  42006  climuzlem  42017  xlimbr  42101  fourierdlem103  42488  fourierdlem104  42489  qndenserrnbllem  42573  2reuimp  43308  ralralimp  43471