Theorem ralrimdv 3133

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3049

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 1912

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

This theorem is referenced by:  ralrimdva  3135  ralrimivv  3176  wefrc  5614  oneqmin  7743  nneneq  9129  cflm  10161  coflim  10172  isf32lem12  10275  axdc3lem2  10362  zorn2lem7  10413  axpre-sup  11081  zmax  12884  zbtwnre  12885  supxrunb2  13261  fzrevral  13555  lcmfdvdsb  16601  islss4  20946  topbas  22925  elcls3  23036  neips  23066  clslp  23101  subbascn  23207  cnpnei  23217  comppfsc  23485  fgss2  23827  fbflim2  23930  alexsubALTlem3  24002  alexsubALTlem4  24003  alexsubALT  24004  metcnp3  24493  mpomulcn  24822  aalioulem3  26288  onsfi  28336  brbtwn2  28962  hial0  31161  hial02  31162  ococss  31352  lnopmi  32059  adjlnop  32145  pjss2coi  32223  pj3cor1i  32268  strlem3a  32311  hstrlem3a  32319  mdbr3  32356  mdbr4  32357  dmdmd  32359  dmdbr3  32364  dmdbr4  32365  dmdbr5  32367  ssmd2  32371  mdslmd1i  32388  mdsymlem7  32468  cdj1i  32492  cdj3lem2b  32496  rankfilimb  35233  sat1el2xp  35549  fvineqsneu  37715  lub0N  39623  glb0N  39627  hlrelat2  39837  snatpsubN  40184  pclclN  40325  pclfinN  40334  pclfinclN  40384  ltrneq2  40582  trlval2  40597  trlord  41003  trintALT  45295  lindslinindsimp2  48927