Theorem 19.23aivv 1296

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 1295	. 2 |- (E.yph -> ps)
3	2	19.23aiv 1295	1 |- (E.xE.yph -> ps)

Syntax hints:   -> wi 3  E.wex 980

This theorem is referenced by:  2mo 1447  cgsex2g 1832  cgsex4g 1833  opabss 2668  dtruALT 2748  copsexg 2792  elopab 2811  opelxp1 3205  elvvuni 3229  optocl 3235  onxpdisj 3241  relop 3275  elreldm 3338  xpnz 3466  unielrel 3514  unixp0 3518  tfrlem7 3917  1stval2 4089  2ndval2 4090  1st2val 4095  2nd2val 4096  th3qlem2 4315  ener 4410  domtr 4415  xpsnen 4435  sbthlem10 4456  abfii4OLD 4564  aceq5lem4 4738  kmlem16 4780  subbasOLD 7644  pjpj0 9255  spanun 9467  osumlem6 9583  5oalem7 9605  3oalem3 9609  stcat 10457  hmeogrp 10538  eloi 10659

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978

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

Copyright terms: Public domain