Theorem el2v 3478

Description: If a proposition is implied by 𝑥 ∈ V and 𝑦 ∈ V (which is true, see vex 3474), then it is true. (Contributed by Peter Mazsa, 13-Oct-2018.)

Hypothesis

Ref	Expression
el2v.1	⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑)

Assertion

Ref	Expression
el2v	⊢ 𝜑

Proof of Theorem el2v

Step	Hyp	Ref	Expression
1		vex 3474	. 2 ⊢ 𝑥 ∈ V
2		vex 3474	. 2 ⊢ 𝑦 ∈ V
3		el2v.1	. 2 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑)
4	1, 2, 3	mp2an 691	1 ⊢ 𝜑

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2099  Vcvv 3470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472

This theorem is referenced by:  codir  6121  dfco2  6244  1st2val  8016  2nd2val  8017  fnmap  8846  enrefnn  9066  unfi  9191  wemappo  9567  wemapsolem  9568  fin23lem26  10343  seqval  14004  hash2exprb  14459  hashle2prv  14466  mreexexlem4d  17621  pmtrrn2  19409  c0snmgmhm  20395  alexsubALTlem4  23948  elqaalem2  26249  seqsval  28155  upgrex  28899  cusgrsize  29262  erclwwlkref  29824  erclwwlksym  29825  erclwwlknref  29873  erclwwlknsym  29874  eclclwwlkn1  29879  gonanegoal  34957  gonarlem  34999  gonar  35000  fmla0disjsuc  35003  fmlasucdisj  35004  mclsppslem  35188  fneer  35832  curunc  37070  matunitlindflem2  37085  vvdifopab  37727  inxprnres  37759  ineccnvmo  37824  alrmomorn  37825  dfcoss2  37880  dfcoss3  37881  cosscnv  37883  cocossss  37903  cnvcosseq  37904  refressn  37910  antisymressn  37911  trressn  37912  rncossdmcoss  37922  symrelcoss3  37932  1cosscnvxrn  37942  cosscnvssid3  37943  cosscnvssid4  37944  coss0  37946  trcoss  37949  trcoss2  37951  erimeq2  38145  dfeldisj3  38186  dfeldisj4  38187  dfantisymrel5  38229  ismrc  42112  en2pr  42968  pr2cv  42969  ovnsubaddlem1  45949  sprsymrelfvlem  46821  sprsymrelf1lem  46822  prprelb  46847  prprspr2  46849  reuprpr  46854  2exopprim  46856  reuopreuprim  46857

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

OSZAR »