Theorem r19.20i2 1700

Description: Inference quantifying both antecedent and consequent.

Hypothesis

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

Assertion

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

Proof of Theorem r19.20i2

Step	Hyp	Ref	Expression
1		r19.20i2.1	. . 3 ⊢ ((x ∈ A → φ) → (x ∈ B → ψ))
2	1	19.20i 990	. 2 ⊢ (∀x(x ∈ A → φ) → ∀x(x ∈ B → ψ))
3		df-ral 1646	. 2 ⊢ (∀x ∈ A φ ↔ ∀x(x ∈ A → φ))
4		df-ral 1646	. 2 ⊢ (∀x ∈ B ψ ↔ ∀x(x ∈ B → ψ))
5	2, 3, 4	3imtr4 219	1 ⊢ (∀x ∈ A φ → ∀x ∈ B ψ)

Syntax hints:   → wi 3  ∀wal 952   ∈ wcel 956  ∀wral 1642

This theorem is referenced by:  r19.20i 1701  ralcom3 1774  tfi 3126  omex 4619  kmlem1 4757  brdom5 4794  brdom4 4795  xrub 6047  seqzeq 6507  cau5i 6874  iserzshft2 7064  clim2serzt 7090  iserzmulc1 7092  isum1p 7161  isumreclt 7165  isummulc1ALT 7168  fsum0diaglem2 7212  basgen2t 7601  sumdmd 10317  dmdbr6at 10319

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973

This theorem depends on definitions:  df-bi 147  df-ral 1646

Copyright terms: Public domain