Theorem r19.20dv2 1709

Description: Inference quantifying both antecedent and consequent.

Hypothesis

Ref	Expression
r19.20dv2.1	⊢ (φ → ((x ∈ A → ψ) → (x ∈ B → χ)))

Assertion

Ref	Expression
r19.20dv2	⊢ (φ → (∀x ∈ A ψ → ∀x ∈ B χ))

Distinct variable group:   φ,x

Proof of Theorem r19.20dv2

Step	Hyp	Ref	Expression
1		r19.20dv2.1	. . 3 ⊢ (φ → ((x ∈ A → ψ) → (x ∈ B → χ)))
2	1	19.20dv 1288	. 2 ⊢ (φ → (∀x(x ∈ A → ψ) → ∀x(x ∈ B → χ)))
3		df-ral 1647	. 2 ⊢ (∀x ∈ A ψ ↔ ∀x(x ∈ A → ψ))
4		df-ral 1647	. 2 ⊢ (∀x ∈ B χ ↔ ∀x(x ∈ B → χ))
5	2, 3, 4	3imtr4g 552	1 ⊢ (φ → (∀x ∈ A ψ → ∀x ∈ B χ))

Syntax hints:   → wi 3  ∀wal 953   ∈ wcel 957  ∀wral 1643

This theorem is referenced by:  ssralv 2111  xrsupexmnf 6031  xrinfmexpnf 6032  xrsupsslem 6033  xrinfmsslem 6034  xrub 6037  fsequb 6468  seqzfveq 6499  fsump1s 6966  fsumcllem 6967  fsum1ps 6971  fsumsplit 6973  fsumadd 6975  fsumcom 6981  fsumrev 6982  fsummulc1 6986  fsumcmp 6993  fsumcmpndx2 6995  fsumabs 6996  climconst 7047  clim2serzt 7087  climserzle 7100  isum1p 7158  iserzgt0 7163  fsum0diaglem2 7209  fsum0diag2 7211  fsum0diag3 7212  fsum0diag4 7213  elcls3 7671  metreslem 7784

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-17 970  ax-4 972  ax-5o 974

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1647

Copyright terms: Public domain