Theorem 19.23ai 746

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

Hypotheses

Ref	Expression
19.23ai.1	⊢ (ψ → ∀xψ)
19.23ai.2	⊢ (φ → ψ)

Assertion

Ref	Expression
19.23ai	⊢ (∃xφ → ψ)

Proof of Theorem 19.23ai

Step	Hyp	Ref	Expression
1		19.23ai.2	. . 3 ⊢ (φ → ψ)
2	1	19.22i 723	. 2 ⊢ (∃xφ → ∃xψ)
3		19.23ai.1	. . 3 ⊢ (ψ → ∀xψ)
4	3	19.9r 718	. 2 ⊢ (ψ ↔ ∃xψ)
5	2, 4	sylibr 175	1 ⊢ (∃xφ → ψ)

Syntax hints:   → wi 2  ∀wal 672  ∃wex 678

This theorem is referenced by:  eqvin.l2 931  19.23aiv 952  moexex 1058  r19.23ai 1283  ceqsex 1370  vtoclgf 1382  vtoclef 1392  vsbcint 1438  sbcel1 1466  sbcel2 1467  copsex2g 1903  mosubop 1911  reucl 1957  opabsb 2114  opelopabg 2115  ralxp 2456  fneu 2728  fv3 2839  tz6.12c 2846  fvopabgf 2874  fvopabnf 2875  fvopab2 2878  zfregcl 3446  scottex 3541  scott0 3542  aceq5lem5 3562  zfcndpow 3762  zfcndreg 3763  zfcndinf 3764  suppsrlem 4015  suppsr3 4018  nn1suc 4435  uzind 4603

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org