Theorem 19.23aivv 1291

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 groups:   ps,x   ps,y

Proof of Theorem 19.23aivv

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

Syntax hints:   -> wi 3  E.wex 977

This theorem is referenced by:  2mo 1440  cgsex2g 1823  cgsex4g 1824  opabss 2658  dtruALT 2738  copsexg 2782  elopab 2800  opelxp1 3195  elvvuni 3219  optocl 3225  onxpdisj 3231  relop 3265  elreldm 3327  xpnz 3452  unielrel 3500  unixp0 3504  tfrlem7 3902  1stval2 4073  2ndval2 4074  1st2val 4079  2nd2val 4080  th3qlem2 4299  ener 4391  domtr 4396  xpsnen 4415  sbthlem10 4436  abfii4 4538  aceq5lem4 4710  kmlem16 4752  subbas 7586  pjpj0 9170  spanun 9382  osumlem6 9500  5oalem7 9522  3oalem3 9526  stcat 10353  hmeogrp 10425  eloi 10503

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain