Theorem ralrimdv 3150

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2104  ∀wral 3059

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3060

This theorem is referenced by:  ralrimdva  3152  ralrimivv  3196  wefrc  5669  oneqmin  7790  nneneq  9211  nneneqOLD  9223  cflm  10247  coflim  10258  isf32lem12  10361  axdc3lem2  10448  zorn2lem7  10499  axpre-sup  11166  zmax  12933  zbtwnre  12934  supxrunb2  13303  fzrevral  13590  lcmfdvdsb  16584  islss4  20717  topbas  22695  elcls3  22807  neips  22837  clslp  22872  subbascn  22978  cnpnei  22988  comppfsc  23256  fgss2  23598  fbflim2  23701  alexsubALTlem3  23773  alexsubALTlem4  23774  alexsubALT  23775  metcnp3  24269  mpomulcn  24605  aalioulem3  26083  brbtwn2  28430  hial0  30622  hial02  30623  ococss  30813  lnopmi  31520  adjlnop  31606  pjss2coi  31684  pj3cor1i  31729  strlem3a  31772  hstrlem3a  31780  mdbr3  31817  mdbr4  31818  dmdmd  31820  dmdbr3  31825  dmdbr4  31826  dmdbr5  31828  ssmd2  31832  mdslmd1i  31849  mdsymlem7  31929  cdj1i  31953  cdj3lem2b  31957  sat1el2xp  34668  fvineqsneu  36595  lub0N  38362  glb0N  38366  hlrelat2  38577  snatpsubN  38924  pmaple  38935  pclclN  39065  pclfinN  39074  pclfinclN  39124  ltrneq2  39322  trlval2  39337  trlord  39743  trintALT  43944  lindslinindsimp2  47231