Theorem 19.23v 1936

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 1579	. 2 ⊢ (𝜓 → ∀𝑥𝜓)
2	1	19.23h 1551	1 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1400  ∃wex 1545

This theorem was proved from axioms:  ax-mp 5  ax-gen 1502  ax-ie2 1547  ax-17 1579

This theorem is referenced by:  19.23vv  1937  equsv  1938  2eu4  2180  gencbval  2871  euind  3013  reuind  3031  snssb  3843  unissb  3960  disjnim  4115  dftr2  4226  ssrelrel  4870  cotr  5164  dffun2  5382  fununi  5444  dff13  5964  acexmidlem2  6072