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  5620  oneqmin  7749  nneneq  9135  cflm  10167  coflim  10178  isf32lem12  10281  axdc3lem2  10368  zorn2lem7  10419  axpre-sup  11087  zmax  12890  zbtwnre  12891  supxrunb2  13267  fzrevral  13561  lcmfdvdsb  16607  islss4  20952  topbas  22951  elcls3  23062  neips  23092  clslp  23127  subbascn  23233  cnpnei  23243  comppfsc  23511  fgss2  23853  fbflim2  23956  alexsubALTlem3  24028  alexsubALTlem4  24029  alexsubALT  24030  metcnp3  24519  mpomulcn  24848  aalioulem3  26315  onsfi  28366  brbtwn2  28992  hial0  31192  hial02  31193  ococss  31383  lnopmi  32090  adjlnop  32176  pjss2coi  32254  pj3cor1i  32299  strlem3a  32342  hstrlem3a  32350  mdbr3  32387  mdbr4  32388  dmdmd  32390  dmdbr3  32395  dmdbr4  32396  dmdbr5  32398  ssmd2  32402  mdslmd1i  32419  mdsymlem7  32499  cdj1i  32523  cdj3lem2b  32527  rankfilimb  35265  sat1el2xp  35581  fvineqsneu  37747  lub0N  39655  glb0N  39659  hlrelat2  39869  snatpsubN  40216  pclclN  40357  pclfinN  40366  pclfinclN  40416  ltrneq2  40614  trlval2  40629  trlord  41035  trintALT  45331  lindslinindsimp2  48957