Theorem ralrimdv 3136

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

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

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 3053

This theorem is referenced by:  ralrimdva  3138  ralrimivv  3179  wefrc  5628  oneqmin  7757  nneneq  9144  cflm  10174  coflim  10185  isf32lem12  10288  axdc3lem2  10375  zorn2lem7  10426  axpre-sup  11094  zmax  12872  zbtwnre  12873  supxrunb2  13249  fzrevral  13542  lcmfdvdsb  16584  islss4  20930  topbas  22933  elcls3  23044  neips  23074  clslp  23109  subbascn  23215  cnpnei  23225  comppfsc  23493  fgss2  23835  fbflim2  23938  alexsubALTlem3  24010  alexsubALTlem4  24011  alexsubALT  24012  metcnp3  24501  mpomulcn  24831  aalioulem3  26315  onsfi  28369  brbtwn2  28996  hial0  31196  hial02  31197  ococss  31387  lnopmi  32094  adjlnop  32180  pjss2coi  32258  pj3cor1i  32303  strlem3a  32346  hstrlem3a  32354  mdbr3  32391  mdbr4  32392  dmdmd  32394  dmdbr3  32399  dmdbr4  32400  dmdbr5  32402  ssmd2  32406  mdslmd1i  32423  mdsymlem7  32503  cdj1i  32527  cdj3lem2b  32531  rankfilimb  35285  sat1el2xp  35601  fvineqsneu  37693  lub0N  39594  glb0N  39598  hlrelat2  39808  snatpsubN  40155  pclclN  40296  pclfinN  40305  pclfinclN  40355  ltrneq2  40553  trlval2  40568  trlord  40974  trintALT  45265  lindslinindsimp2  48852