Theorem ralrimdv 3169

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 27-May-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Dec-2019.)

Hypothesis

Ref	Expression
ralrimdv.1	⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒)))

Assertion

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

Distinct variable groups:   𝜑,𝑥   𝜓,𝑥

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

Proof of Theorem ralrimdv

Step	Hyp	Ref	Expression
1		ralrimdv.1	. . . 4 ⊢ (𝜑 → (𝜓 → (𝑥 ∈ 𝐴 → 𝜒)))
2	1	imp 411	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ 𝐴 → 𝜒))
3	2	ralrimiv 3162	. 2 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜒)
4	3	ex 417	1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3086

This theorem is referenced by:  ralrimdva  3171  ralrimivv  3212  wefrc  5656  oneqmin  7799  nneneq  9190  cflm  10233  coflim  10245  isf32lem12  10348  axdc3lem2  10435  zorn2lem7  10486  axpre-sup  11154  zmax  12969  zbtwnre  12970  supxrunb2  13346  fzrevral  13640  lcmfdvdsb  16701  islss4  21061  topbas  23098  elcls3  23209  neips  23239  clslp  23274  subbascn  23380  cnpnei  23390  comppfsc  23658  fgss2  24000  fbflim2  24103  alexsubALTlem3  24175  alexsubALTlem4  24176  alexsubALT  24177  metcnp3  24666  mpomulcn  24995  aalioulem3  26464  onsfi  28515  brbtwn2  29196  hial0  31395  hial02  31396  ococss  31586  lnopmi  32293  adjlnop  32379  pjss2coi  32457  pj3cor1i  32502  strlem3a  32545  hstrlem3a  32553  mdbr3  32590  mdbr4  32591  dmdmd  32593  dmdbr3  32598  dmdbr4  32599  dmdbr5  32601  ssmd2  32605  mdslmd1i  32622  mdsymlem7  32702  cdj1i  32726  cdj3lem2b  32730  rankfilimb  35439  sat1el2xp  35804  fvineqsneu  37980  lub0N  39888  glb0N  39892  hlrelat2  40102  snatpsubN  40449  pclclN  40590  pclfinN  40599  pclfinclN  40649  ltrneq2  40847  trlval2  40862  trlord  41268  trintALT  45516  lindslinindsimp2  49163