Theorem 19.23ai 1412

Description: Inference from Theorem 19.23 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 13-May-2011.)

Hypotheses

Ref	Expression
19.23ai.1	|- (ps -> A.xps)
19.23ai.2	|- (ph -> ps)

Assertion

Ref	Expression
19.23ai	|- (E.xph -> ps)

Proof of Theorem 19.23ai

Step	Hyp	Ref	Expression
1		19.23ai.1	. . 3 |- (ps -> A.xps)
2	1	19.23 1411	. 2 |- (A.x(ph -> ps) <-> (E.xph -> ps))
3		19.23ai.2	. 2 |- (ph -> ps)
4	2, 3	mpgbi 1333	1 |- (E.xph -> ps)

Syntax hints:   -> wi 3  A.wal 1296  E.wex 1326

This theorem is referenced by:  19.41 1448  equs5a 1566  sb5rf 1633  sb5rfOLD 1634  equid1 1646  equvin 1652  19.23aiv 1674  euan 1827  moexex 1841  r19.23aiOLD 2210  ceqsex 2324  vtoclgf 2345  vtoclef 2358  moi2 2435  moi 2436  sbhypf 2452  sbcel1gvOLD 2511  sbcel2gvOLD 2513  csbhypf 2572  reucl 3213  intab 3247  sbcbrgOLD 3391  copsexg 3537  copsex2g 3539  opelopabsbOLD 3565  eufromeq1 3828  eufromeq5 3832  alxfr 3836  ralxp 4041  ralxpf 4043  dmcoss 4211  csbima12g 4276  fneuOLD 4518  fv3 4690  tz6.12c 4697  csbfv12g 4699  fvopab2 4754  fvopab5 4756  csboprgOLD 4911  dfoprab5sf 5058  ordtype 5691  zfregcl 5697  scottex 5846  scott0 5847  omsubsdomlem2 5880  aceq5lem5 5901  zfcndpow 6120  zfcndreg 6121  zfcndinf 6122  suppsrlem 6373  suppsr3 6376  csbneggOLD 6521  nn1suc 7122  uzindOLD 7420  isumcl 8470  oprabopabf 10157  bnj65 13202  bnj578 13291  bnj607 13304  bnj900 13325  exisym1 14248  stoig2b 14906  subtr 15352  subtr2 15353  ordtypeOLD 15382  omsubsdomlem2OLD 15389  ceqsex3OLD 16249

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain