Theorem ralrimdv 3131

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045

This theorem is referenced by:  ralrimdva  3133  ralrimivv  3176  wefrc  5625  oneqmin  7756  nneneq  9147  cflm  10179  coflim  10190  isf32lem12  10293  axdc3lem2  10380  zorn2lem7  10431  axpre-sup  11098  zmax  12880  zbtwnre  12881  supxrunb2  13256  fzrevral  13549  lcmfdvdsb  16589  islss4  20900  topbas  22892  elcls3  23003  neips  23033  clslp  23068  subbascn  23174  cnpnei  23184  comppfsc  23452  fgss2  23794  fbflim2  23897  alexsubALTlem3  23969  alexsubALTlem4  23970  alexsubALT  23971  metcnp3  24461  mpomulcn  24791  aalioulem3  26275  onsfi  28287  brbtwn2  28885  hial0  31081  hial02  31082  ococss  31272  lnopmi  31979  adjlnop  32065  pjss2coi  32143  pj3cor1i  32188  strlem3a  32231  hstrlem3a  32239  mdbr3  32276  mdbr4  32277  dmdmd  32279  dmdbr3  32284  dmdbr4  32285  dmdbr5  32287  ssmd2  32291  mdslmd1i  32308  mdsymlem7  32388  cdj1i  32412  cdj3lem2b  32416  sat1el2xp  35359  fvineqsneu  37392  lub0N  39175  glb0N  39179  hlrelat2  39390  snatpsubN  39737  pmaple  39748  pclclN  39878  pclfinN  39887  pclfinclN  39937  ltrneq2  40135  trlval2  40150  trlord  40556  trintALT  44863  lindslinindsimp2  48445