Theorem ralrimdv 3164

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3081

This theorem is used by:  ralrimdva  3166  ralrimivv  3207  wefrc  5649  oneqmin  7835  nneneq  9246  cflm  10351  coflim  10363  isf32lem12  10466  axdc3lem2  10553  zorn2lem7  10604  axpre-sup  11278  zmax  13096  zbtwnre  13097  supxrunb2  13474  fzrevral  13770  lcmfdvdsb  16844  islss4  21264  topbas  23317  elcls3  23428  neips  23458  clslp  23493  subbascn  23599  cnpnei  23609  comppfsc  23878  fgss2  24220  fbflim2  24323  alexsubALTlem3  24395  alexsubALTlem4  24396  alexsubALT  24397  metcnp3  24886  mpomulcn  25215  aalioulem3  26688  onsfi  28769  brbtwn2  29510  hial0  31731  hial02  31732  ococss  31922  lnopmi  32629  adjlnop  32715  pjss2coi  32793  pj3cor1i  32838  strlem3a  32881  hstrlem3a  32889  mdbr3  32926  mdbr4  32927  dmdmd  32929  dmdbr3  32934  dmdbr4  32935  dmdbr5  32937  ssmd2  32941  mdslmd1i  32958  mdsymlem7  33038  cdj1i  33062  cdj3lem2b  33066  rankfilimb  35809  sat1el2xp  36310  fvineqsneu  38525  lub0N  40437  glb0N  40441  hlrelat2  40651  snatpsubN  40998  pclclN  41139  pclfinN  41148  pclfinclN  41198  ltrneq2  41396  trlval2  41411  trlord  41817  trintALT  46052  lindslinindsimp2  49778