Theorem 19.23v 1932

Description: Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.)

Assertion

Ref	Expression
19.23v	⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Distinct variable group:   𝜓,𝑥

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem 19.23v

Step	Hyp	Ref	Expression
1		ax-17 1575	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
2	1	19.23h 1547	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1396  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem is referenced by:  19.23vv  1933  equsv  1934  2eu4  2176  gencbval  2865  euind  3007  reuind  3025  snssb  3832  unissb  3949  disjnim  4104  dftr2  4215  ssrelrel  4855  cotr  5149  dffun2  5367  fununi  5429  dff13  5947  acexmidlem2  6055