Theorem ralrimdv 2950

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

Syntax hints:   → wi 4   ∧ wa 382   ∈ wcel 1976  ∀wral 2895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826

This theorem depends on definitions:  df-bi 195  df-an 384  df-ral 2900

This theorem is referenced by:  ralrimdva  2951  ralrimivv  2952  wefrc  5022  oneqmin  6875  nneneq  8006  cflm  8933  coflim  8944  isf32lem12  9047  axdc3lem2  9134  zorn2lem7  9185  axpre-sup  9847  zmax  11620  zbtwnre  11621  supxrunb2  11981  fzrevral  12252  islss4  18732  topbas  20535  elcls3  20645  neips  20675  clslp  20710  subbascn  20816  cnpnei  20826  comppfsc  21093  fgss2  21436  fbflim2  21539  alexsubALTlem3  21611  alexsubALTlem4  21612  alexsubALT  21613  metcnp3  22103  aalioulem3  23838  brbtwn2  25531  hial0  27177  hial02  27178  ococss  27370  lnopmi  28077  adjlnop  28163  pjss2coi  28241  pj3cor1i  28286  strlem3a  28329  hstrlem3a  28337  mdbr3  28374  mdbr4  28375  dmdmd  28377  dmdbr3  28382  dmdbr4  28383  dmdbr5  28385  ssmd2  28389  mdslmd1i  28406  mdsymlem7  28486  cdj1i  28510  cdj3lem2b  28514  lub0N  33318  glb0N  33322  hlrelat2  33531  snatpsubN  33878  pmaple  33889  pclclN  34019  pclfinN  34028  pclfinclN  34078  ltrneq2  34276  trlval2  34292  trlord  34699  trintALT  37963  lindslinindsimp2  42068