Metamath Proof Explorer
Description: New way ( elv , and the theorems beginning with "el2v" or "el3v") to
shorten some proofs. (Contributed by Peter Mazsa, 23Oct2018)


Ref 
Expression 

Hypothesis 
el2v1.1 
$${\u22a2}\left({x}\in \mathrm{V}\wedge {\phi}\right)\to {\psi}$$ 

Assertion 
el2v1 
$${\u22a2}{\phi}\to {\psi}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

el2v1.1 
$${\u22a2}\left({x}\in \mathrm{V}\wedge {\phi}\right)\to {\psi}$$ 
2 

vex 
$${\u22a2}{x}\in \mathrm{V}$$ 
3 
2 1

mpan 
$${\u22a2}{\phi}\to {\psi}$$ 