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

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

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