Theorem ralrimdv 3132

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

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

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 3046

This theorem is referenced by:  ralrimdva  3134  ralrimivv  3179  wefrc  5635  oneqmin  7779  nneneq  9176  cflm  10210  coflim  10221  isf32lem12  10324  axdc3lem2  10411  zorn2lem7  10462  axpre-sup  11129  zmax  12911  zbtwnre  12912  supxrunb2  13287  fzrevral  13580  lcmfdvdsb  16620  islss4  20875  topbas  22866  elcls3  22977  neips  23007  clslp  23042  subbascn  23148  cnpnei  23158  comppfsc  23426  fgss2  23768  fbflim2  23871  alexsubALTlem3  23943  alexsubALTlem4  23944  alexsubALT  23945  metcnp3  24435  mpomulcn  24765  aalioulem3  26249  onsfi  28254  brbtwn2  28839  hial0  31038  hial02  31039  ococss  31229  lnopmi  31936  adjlnop  32022  pjss2coi  32100  pj3cor1i  32145  strlem3a  32188  hstrlem3a  32196  mdbr3  32233  mdbr4  32234  dmdmd  32236  dmdbr3  32241  dmdbr4  32242  dmdbr5  32244  ssmd2  32248  mdslmd1i  32265  mdsymlem7  32345  cdj1i  32369  cdj3lem2b  32373  sat1el2xp  35373  fvineqsneu  37406  lub0N  39189  glb0N  39193  hlrelat2  39404  snatpsubN  39751  pmaple  39762  pclclN  39892  pclfinN  39901  pclfinclN  39951  ltrneq2  40149  trlval2  40164  trlord  40570  trintALT  44877  lindslinindsimp2  48456