Theorem ralrimdv 3144

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3054

This theorem is referenced by:  ralrimdva  3146  ralrimivv  3190  wefrc  5661  oneqmin  7782  nneneq  9206  nneneqOLD  9218  cflm  10242  coflim  10253  isf32lem12  10356  axdc3lem2  10443  zorn2lem7  10494  axpre-sup  11161  zmax  12927  zbtwnre  12928  supxrunb2  13297  fzrevral  13584  lcmfdvdsb  16579  islss4  20801  topbas  22799  elcls3  22911  neips  22941  clslp  22976  subbascn  23082  cnpnei  23092  comppfsc  23360  fgss2  23702  fbflim2  23805  alexsubALTlem3  23877  alexsubALTlem4  23878  alexsubALT  23879  metcnp3  24373  mpomulcn  24709  aalioulem3  26190  brbtwn2  28635  hial0  30827  hial02  30828  ococss  31018  lnopmi  31725  adjlnop  31811  pjss2coi  31889  pj3cor1i  31934  strlem3a  31977  hstrlem3a  31985  mdbr3  32022  mdbr4  32023  dmdmd  32025  dmdbr3  32030  dmdbr4  32031  dmdbr5  32033  ssmd2  32037  mdslmd1i  32054  mdsymlem7  32134  cdj1i  32158  cdj3lem2b  32162  sat1el2xp  34861  fvineqsneu  36783  lub0N  38553  glb0N  38557  hlrelat2  38768  snatpsubN  39115  pmaple  39126  pclclN  39256  pclfinN  39265  pclfinclN  39315  ltrneq2  39513  trlval2  39528  trlord  39934  trintALT  44156  lindslinindsimp2  47357