Theorem ralrimdv 3158

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  ralrimdva  3160  ralrimivv  3206  wefrc  5694  oneqmin  7836  nneneq  9272  nneneqOLD  9284  cflm  10319  coflim  10330  isf32lem12  10433  axdc3lem2  10520  zorn2lem7  10571  axpre-sup  11238  zmax  13010  zbtwnre  13011  supxrunb2  13382  fzrevral  13669  lcmfdvdsb  16690  islss4  20983  topbas  23000  elcls3  23112  neips  23142  clslp  23177  subbascn  23283  cnpnei  23293  comppfsc  23561  fgss2  23903  fbflim2  24006  alexsubALTlem3  24078  alexsubALTlem4  24079  alexsubALT  24080  metcnp3  24574  mpomulcn  24910  aalioulem3  26394  brbtwn2  28938  hial0  31134  hial02  31135  ococss  31325  lnopmi  32032  adjlnop  32118  pjss2coi  32196  pj3cor1i  32241  strlem3a  32284  hstrlem3a  32292  mdbr3  32329  mdbr4  32330  dmdmd  32332  dmdbr3  32337  dmdbr4  32338  dmdbr5  32340  ssmd2  32344  mdslmd1i  32361  mdsymlem7  32441  cdj1i  32465  cdj3lem2b  32469  sat1el2xp  35347  fvineqsneu  37377  lub0N  39145  glb0N  39149  hlrelat2  39360  snatpsubN  39707  pmaple  39718  pclclN  39848  pclfinN  39857  pclfinclN  39907  ltrneq2  40105  trlval2  40120  trlord  40526  trintALT  44852  lindslinindsimp2  48192