Theorem ralrimdv 3111

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ral 3068

This theorem is referenced by:  ralrimdva  3112  ralrimivv  3113  wefrc  5574  oneqmin  7627  nneneq  8896  cflm  9937  coflim  9948  isf32lem12  10051  axdc3lem2  10138  zorn2lem7  10189  axpre-sup  10856  zmax  12614  zbtwnre  12615  supxrunb2  12983  fzrevral  13270  lcmfdvdsb  16276  islss4  20139  topbas  22030  elcls3  22142  neips  22172  clslp  22207  subbascn  22313  cnpnei  22323  comppfsc  22591  fgss2  22933  fbflim2  23036  alexsubALTlem3  23108  alexsubALTlem4  23109  alexsubALT  23110  metcnp3  23602  aalioulem3  25399  brbtwn2  27176  hial0  29365  hial02  29366  ococss  29556  lnopmi  30263  adjlnop  30349  pjss2coi  30427  pj3cor1i  30472  strlem3a  30515  hstrlem3a  30523  mdbr3  30560  mdbr4  30561  dmdmd  30563  dmdbr3  30568  dmdbr4  30569  dmdbr5  30571  ssmd2  30575  mdslmd1i  30592  mdsymlem7  30672  cdj1i  30696  cdj3lem2b  30700  sat1el2xp  33241  fvineqsneu  35509  lub0N  37130  glb0N  37134  hlrelat2  37344  snatpsubN  37691  pmaple  37702  pclclN  37832  pclfinN  37841  pclfinclN  37891  ltrneq2  38089  trlval2  38104  trlord  38510  trintALT  42390  lindslinindsimp2  45692