Description: If a proposition is implied by x e. _V (which is true, see vex ), then it is true. (Contributed by Peter Mazsa, 13Oct2018)
Ref  Expression  

Hypothesis  elv.1   ( x e. _V > ph ) 

Assertion  elv   ph 
Step  Hyp  Ref  Expression 

1  elv.1   ( x e. _V > ph ) 

2  vex   x e. _V 

3  2 1  axmp   ph 