Theorem ralrimdv 3152

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ral 3062

This theorem is referenced by:  ralrimdva  3154  ralrimivv  3198  wefrc  5669  oneqmin  7784  nneneq  9205  nneneqOLD  9217  cflm  10241  coflim  10252  isf32lem12  10355  axdc3lem2  10442  zorn2lem7  10493  axpre-sup  11160  zmax  12925  zbtwnre  12926  supxrunb2  13295  fzrevral  13582  lcmfdvdsb  16576  islss4  20565  topbas  22466  elcls3  22578  neips  22608  clslp  22643  subbascn  22749  cnpnei  22759  comppfsc  23027  fgss2  23369  fbflim2  23472  alexsubALTlem3  23544  alexsubALTlem4  23545  alexsubALT  23546  metcnp3  24040  aalioulem3  25838  brbtwn2  28152  hial0  30342  hial02  30343  ococss  30533  lnopmi  31240  adjlnop  31326  pjss2coi  31404  pj3cor1i  31449  strlem3a  31492  hstrlem3a  31500  mdbr3  31537  mdbr4  31538  dmdmd  31540  dmdbr3  31545  dmdbr4  31546  dmdbr5  31548  ssmd2  31552  mdslmd1i  31569  mdsymlem7  31649  cdj1i  31673  cdj3lem2b  31677  sat1el2xp  34358  mpomulcn  35150  fvineqsneu  36280  lub0N  38047  glb0N  38051  hlrelat2  38262  snatpsubN  38609  pmaple  38620  pclclN  38750  pclfinN  38759  pclfinclN  38809  ltrneq2  39007  trlval2  39022  trlord  39428  trintALT  43627  lindslinindsimp2  47097