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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∀wral 3106

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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ral 3111

This theorem is referenced by:  ralrimdva  3154  ralrimivv  3155  wefrc  5513  oneqmin  7500  nneneq  8684  cflm  9661  coflim  9672  isf32lem12  9775  axdc3lem2  9862  zorn2lem7  9913  axpre-sup  10580  zmax  12333  zbtwnre  12334  supxrunb2  12701  fzrevral  12987  lcmfdvdsb  15977  islss4  19727  topbas  21577  elcls3  21688  neips  21718  clslp  21753  subbascn  21859  cnpnei  21869  comppfsc  22137  fgss2  22479  fbflim2  22582  alexsubALTlem3  22654  alexsubALTlem4  22655  alexsubALT  22656  metcnp3  23147  aalioulem3  24930  brbtwn2  26699  hial0  28885  hial02  28886  ococss  29076  lnopmi  29783  adjlnop  29869  pjss2coi  29947  pj3cor1i  29992  strlem3a  30035  hstrlem3a  30043  mdbr3  30080  mdbr4  30081  dmdmd  30083  dmdbr3  30088  dmdbr4  30089  dmdbr5  30091  ssmd2  30095  mdslmd1i  30112  mdsymlem7  30192  cdj1i  30216  cdj3lem2b  30220  sat1el2xp  32739  fvineqsneu  34828  lub0N  36485  glb0N  36489  hlrelat2  36699  snatpsubN  37046  pmaple  37057  pclclN  37187  pclfinN  37196  pclfinclN  37246  ltrneq2  37444  trlval2  37459  trlord  37865  trintALT  41587  lindslinindsimp2  44872