Theorem ralrimdv 3153

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∀wral 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063

This theorem is referenced by:  ralrimdva  3155  ralrimivv  3199  wefrc  5671  oneqmin  7788  nneneq  9209  nneneqOLD  9221  cflm  10245  coflim  10256  isf32lem12  10359  axdc3lem2  10446  zorn2lem7  10497  axpre-sup  11164  zmax  12929  zbtwnre  12930  supxrunb2  13299  fzrevral  13586  lcmfdvdsb  16580  islss4  20573  topbas  22475  elcls3  22587  neips  22617  clslp  22652  subbascn  22758  cnpnei  22768  comppfsc  23036  fgss2  23378  fbflim2  23481  alexsubALTlem3  23553  alexsubALTlem4  23554  alexsubALT  23555  metcnp3  24049  aalioulem3  25847  brbtwn2  28163  hial0  30355  hial02  30356  ococss  30546  lnopmi  31253  adjlnop  31339  pjss2coi  31417  pj3cor1i  31462  strlem3a  31505  hstrlem3a  31513  mdbr3  31550  mdbr4  31551  dmdmd  31553  dmdbr3  31558  dmdbr4  31559  dmdbr5  31561  ssmd2  31565  mdslmd1i  31582  mdsymlem7  31662  cdj1i  31686  cdj3lem2b  31690  sat1el2xp  34370  mpomulcn  35162  fvineqsneu  36292  lub0N  38059  glb0N  38063  hlrelat2  38274  snatpsubN  38621  pmaple  38632  pclclN  38762  pclfinN  38771  pclfinclN  38821  ltrneq2  39019  trlval2  39034  trlord  39440  trintALT  43642  lindslinindsimp2  47144