MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  el2v Structured version   Visualization version   GIF version

Theorem el2v 3404
Description: If a proposition is implied by 𝑥 ∈ V and 𝑦 ∈ V (which is true, see vex 3401), 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
StepHypRef Expression
1 vex 3401 . 2 𝑥 ∈ V
2 vex 3401 . 2 𝑦 ∈ V
3 el2v.1 . 2 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑)
41, 2, 3mp2an 682 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  wcel 2107  Vcvv 3398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-tru 1605  df-ex 1824  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-v 3400
This theorem is referenced by:  vvdifopab  34664  inxprnres  34696  ineccnvmo  34755  alrmomorn  34756  dfcoss2  34804  dfcoss3  34805  cocossss  34824  cnvcosseq  34825  rncossdmcoss  34838  symrelcoss3  34848  1cosscnvxrn  34858  cosscnvssid3  34859  cosscnvssid4  34860  coss0  34862  trcoss  34865  trcoss2  34867  prprelb  42465  prprspr2  42467
  Copyright terms: Public domain W3C validator