Theorem 19.21aiv 943

Description: Inference from Theorem 19.21 of [Margaris] p. 90.

Hypothesis

Ref	Expression
19.21aiv.1	⊢ (φ → ψ)

Assertion

Ref	Expression
19.21aiv	⊢ (φ → ∀xψ)

Distinct variable group(s):   φ,x

Proof of Theorem 19.21aiv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 ⊢ (φ → ∀xφ)
2		19.21aiv.1	. 2 ⊢ (φ → ψ)
3	1, 2	19.21ai 740	1 ⊢ (φ → ∀xψ)

Syntax hints:   → wi 2  ∀wal 672

This theorem is referenced by:  19.21aivv 944  cleqrd 1100  biabrdv 1184  biabldv 1185  moeq3 1432  sbc2or 1454  sbcie 1455  bisbcdv 1468  zfaus 1480  ssrdv 1509  reuss 1577  disjsn 1836  uniss 1936  intss 1983  iunss1 2002  ssiun 2018  ssopab2 2119  onminex 2275  limom 2387  cotr 2625  funco 2696  funun 2700  fununi 2705  funcnvuni 2706  fvopabn 2873  fopab2 2891  iunon 2947  iinon 2948  erdisj 3223  mapss 3270  pw2en 3348  fiint 3445  sucprcreg 3451  aceq3 3556  aceq5 3563  aceq6b 3565  kmlem1 3580  kmlem6 3585  kmlem12 3591  cfub 3703  cflim 3704  cflecard 3707  1pr 3911  reclem2pr 3951  suppr 3957

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925

metamath.org