Theorem 19.23ai 1040

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 1016	. 2 |- (E.xph -> E.xps)
3		19.23ai.1	. . 3 |- (ps -> A.xps)
4	3	19.9 1012	. 2 |- (E.xps <-> ps)
5	2, 4	sylib 198	1 |- (E.xph -> ps)

Syntax hints:   -> wi 3  A.wal 950  E.wex 956

This theorem is referenced by:  equs5a 1181  sb5rf 1243  equid1 1253  equvin 1257  19.23aiv 1277  moexex 1415  r19.23ai 1718  ceqsex 1809  vtoclgf 1821  vtoclef 1832  moi 1896  sbhypf 1910  sbhyp 1911  sbcel1gv 1951  sbcel2gv 1952  intab 2528  sbcbrg 2630  copsex2g 2760  opabsb 2777  reucl 2848  alxfr 2859  ralxp 3180  ralxpf 3182  csbima12g 3364  fneu 3532  fv3 3672  tz6.12c 3679  csbfv12g 3681  fvopab4gf 3720  fvopabgf 3726  fvopabnf 3727  fvopab2 3730  fvopab5 3732  csboprg 3925  oprabval2gf 3965  zfregcl 4519  scottex 4640  scott0 4641  aceq5lem5 4663  zfcndpow 4891  zfcndreg 4892  zfcndinf 4893  suppsrlem 5144  suppsr3 5147  csbnegg 5287  nn1suc 5838  uzindOLD 6107  fsum1f 6896  fsump1f 6900  isumclt 7095

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955

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

Copyright terms: Public domain