Theorem exlimi 2205

Description: Inference associated with 19.23 2199. See exlimiv 1925 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)

Hypotheses

Ref	Expression
exlimi.1	⊢ Ⅎ𝑥𝜓
exlimi.2	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
exlimi	⊢ (∃𝑥𝜑 → 𝜓)

Proof of Theorem exlimi

Step	Hyp	Ref	Expression
1		exlimi.1	. . 3 ⊢ Ⅎ𝑥𝜓
2	1	19.23 2199	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
3		exlimi.2	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	mpgbi 1792	1 ⊢ (∃𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4  ∃wex 1773  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778

This theorem is referenced by:  sbalex  2230  equsexv  2254  equs5av  2265  exlimih  2278  equs5aALT  2357  equs5eALT  2358  equsex  2411  exdistrf  2440  equs5a  2450  equs5e  2451  dfmoeu  2524  moanim  2608  euan  2609  moexexlem  2614  2eu6  2645  ceqsexOLD  3514  sbhypfOLD  3529  vtoclef  3540  vtoclgf  3547  vtoclg1f  3548  rspn0OLD  4347  reusv2lem1  5390  copsexgw  5484  copsexg  5485  copsex2gOLD  5488  rexopabb  5522  0nelopabOLD  5562  ralxpf  5841  dmcoss  5966  fv3  6908  opabiota  6974  oprabidw  7445  zfregcl  9615  scottex  9906  scott0  9907  dfac5lem5  10148  zfcndpow  10637  zfcndreg  10638  zfcndinf  10639  reclem2pr  11069  mreiincl  17573  brabgaf  32415  cnvoprabOLD  32519  bnj607  34576  bnj900  34589  exisym1  35937  exlimii  36337  bj-exlimmpi  36419  bj-exlimmpbi  36420  bj-exlimmpbir  36421  dihglblem5  40799  tworepnotupword  46307  eu2ndop1stv  46540  pgind  48232

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »