Theorem 19.23ai 1064

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

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.2	. . 3 |- (ph -> ps)
2	1	19.22i 1040	. 2 |- (E.xph -> E.xps)
3		19.23ai.1	. . 3 |- (ps -> A.xps)
4	3	19.9 1036	. 2 |- (E.xps <-> ps)
5	2, 4	sylib 198	1 |- (E.xph -> ps)

Syntax hints:   -> wi 3  A.wal 954  E.wex 980

This theorem is referenced by:  equs5a 1197  sb5rf 1259  equid1 1269  equvin 1275  19.23aiv 1295  moexex 1438  r19.23ai 1742  ceqsex 1834  vtoclgf 1846  vtoclef 1857  moi2 1924  moi 1925  sbhypf 1939  sbhyp 1940  sbcel1gv 1980  sbcel2gv 1981  intab 2560  sbcbrg 2662  copsex2g 2793  opabsb 2815  reucl 2885  alxfr 2896  ralxp 3218  ralxpf 3220  csbima12g 3413  fneu 3592  fv3 3733  tz6.12c 3740  csbfv12g 3742  fvopab4gf 3781  fvopabgf 3787  fvopabnf 3788  fvopab2 3791  fvopab5 3793  csboprg 3986  oprabval2gf 4026  zfregcl 4595  scottex 4716  scott0 4717  aceq5lem5 4739  zfcndpow 4968  zfcndreg 4969  zfcndinf 4970  suppsrlem 5221  suppsr3 5224  csbnegg 5364  nn1suc 5939  uzindOLD 6208  fsum1f 7007  fsump1f 7011  isumclt 7209

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  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