Theorem ralrimdv 3131

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 406	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝑥 ∈ 𝐴 → 𝜒))
3	2	ralrimiv 3124	. 2 ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥 ∈ 𝐴 𝜒)
4	3	ex 412	1 ⊢ (𝜑 → (𝜓 → ∀𝑥 ∈ 𝐴 𝜒))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045

This theorem is referenced by:  ralrimdva  3133  ralrimivv  3176  wefrc  5625  oneqmin  7756  nneneq  9147  cflm  10181  coflim  10192  isf32lem12  10295  axdc3lem2  10382  zorn2lem7  10433  axpre-sup  11100  zmax  12882  zbtwnre  12883  supxrunb2  13258  fzrevral  13551  lcmfdvdsb  16590  islss4  20901  topbas  22893  elcls3  23004  neips  23034  clslp  23069  subbascn  23175  cnpnei  23185  comppfsc  23453  fgss2  23795  fbflim2  23898  alexsubALTlem3  23970  alexsubALTlem4  23971  alexsubALT  23972  metcnp3  24462  mpomulcn  24792  aalioulem3  26276  onsfi  28288  brbtwn2  28886  hial0  31082  hial02  31083  ococss  31273  lnopmi  31980  adjlnop  32066  pjss2coi  32144  pj3cor1i  32189  strlem3a  32232  hstrlem3a  32240  mdbr3  32277  mdbr4  32278  dmdmd  32280  dmdbr3  32285  dmdbr4  32286  dmdbr5  32288  ssmd2  32292  mdslmd1i  32309  mdsymlem7  32389  cdj1i  32413  cdj3lem2b  32417  sat1el2xp  35360  fvineqsneu  37393  lub0N  39176  glb0N  39180  hlrelat2  39391  snatpsubN  39738  pmaple  39749  pclclN  39879  pclfinN  39888  pclfinclN  39938  ltrneq2  40136  trlval2  40151  trlord  40557  trintALT  44864  lindslinindsimp2  48446