Description: If a proposition is implied by z e. _V (which is true, see vex ) and two other antecedents, then it is implied by these other antecedents. (Contributed by Peter Mazsa, 16-Oct-2020)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | el3v3.1 | |- ( ( ph /\ ps /\ z e. _V ) -> th ) |
|
| Assertion | el3v3 | |- ( ( ph /\ ps ) -> th ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | el3v3.1 | |- ( ( ph /\ ps /\ z e. _V ) -> th ) |
|
| 2 | vex | |- z e. _V |
|
| 3 | 2 1 | mp3an3 | |- ( ( ph /\ ps ) -> th ) |