Theorem ralrimdv 3130

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  ralrimdva  3132  ralrimivv  3173  wefrc  5608  oneqmin  7733  nneneq  9115  cflm  10141  coflim  10152  isf32lem12  10255  axdc3lem2  10342  zorn2lem7  10393  axpre-sup  11060  zmax  12843  zbtwnre  12844  supxrunb2  13219  fzrevral  13512  lcmfdvdsb  16554  islss4  20895  topbas  22887  elcls3  22998  neips  23028  clslp  23063  subbascn  23169  cnpnei  23179  comppfsc  23447  fgss2  23789  fbflim2  23892  alexsubALTlem3  23964  alexsubALTlem4  23965  alexsubALT  23966  metcnp3  24455  mpomulcn  24785  aalioulem3  26269  onsfi  28283  brbtwn2  28883  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  rankfilimb  35113  sat1el2xp  35423  fvineqsneu  37455  lub0N  39287  glb0N  39291  hlrelat2  39501  snatpsubN  39848  pmaple  39859  pclclN  39989  pclfinN  39998  pclfinclN  40048  ltrneq2  40246  trlval2  40261  trlord  40667  trintALT  44972  lindslinindsimp2  48563