Theorem ralrimdv 3127

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

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 1910

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

This theorem is referenced by:  ralrimdva  3129  ralrimivv  3170  wefrc  5613  oneqmin  7736  nneneq  9120  cflm  10144  coflim  10155  isf32lem12  10258  axdc3lem2  10345  zorn2lem7  10396  axpre-sup  11063  zmax  12846  zbtwnre  12847  supxrunb2  13222  fzrevral  13515  lcmfdvdsb  16554  islss4  20865  topbas  22857  elcls3  22968  neips  22998  clslp  23033  subbascn  23139  cnpnei  23149  comppfsc  23417  fgss2  23759  fbflim2  23862  alexsubALTlem3  23934  alexsubALTlem4  23935  alexsubALT  23936  metcnp3  24426  mpomulcn  24756  aalioulem3  26240  onsfi  28254  brbtwn2  28854  hial0  31050  hial02  31051  ococss  31241  lnopmi  31948  adjlnop  32034  pjss2coi  32112  pj3cor1i  32157  strlem3a  32200  hstrlem3a  32208  mdbr3  32245  mdbr4  32246  dmdmd  32248  dmdbr3  32253  dmdbr4  32254  dmdbr5  32256  ssmd2  32260  mdslmd1i  32277  mdsymlem7  32357  cdj1i  32381  cdj3lem2b  32385  sat1el2xp  35372  fvineqsneu  37405  lub0N  39188  glb0N  39192  hlrelat2  39402  snatpsubN  39749  pmaple  39760  pclclN  39890  pclfinN  39899  pclfinclN  39949  ltrneq2  40147  trlval2  40162  trlord  40568  trintALT  44874  lindslinindsimp2  48468