Theorem 19.23aivv 953

Description: Inference from Theorem 19.23 of [Margaris] p. 90.

Hypothesis

Ref	Expression
19.23aivv.1	|- (ph -> ps)

Assertion

Ref	Expression
19.23aivv	|- (E.xE.yph -> ps)

Distinct variable group(s):   ps,x   ps,y

Proof of Theorem 19.23aivv

Step	Hyp	Ref	Expression
1		19.23aivv.1	. . 3 |- (ph -> ps)
2	1	19.23aiv 952	. 2 |- (E.yph -> ps)
3	2	19.23aiv 952	1 |- (E.xE.yph -> ps)

Syntax hints:   -> wi 2  E.wex 678

This theorem is referenced by:  cgsex2g 1368  cgsex4g 1369  copsexg 1902  opabss 2100  elopab 2110  opelxpex 2445  optocl 2469  onxpdisj 2476  elreldm 2554  tfrlem7 2955  tfrlem8 2956  1st2val 3097  th3qlem2 3251  ener 3313  domtr 3320  xpsnen 3339  sbthlem10 3358  aceq5lem4 3561  kmlem16 3595  pjpj0 5259  spanun 5450  osumlem6 5535  5oalem7 5550  3oalem3 5554

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org