Theorem 19.21adv 1666

Description: Deduction from Theorem 19.21 of [Margaris] p. 90.

Hypothesis

Ref	Expression
19.21adv.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
19.21adv	|- (ph -> (ps -> A.xch))

Distinct variable groups:   ph,x   ps,x

Proof of Theorem 19.21adv

Step	Hyp	Ref	Expression
1		ax-17 1317	. 2 |- (ph -> A.xph)
2		ax-17 1317	. 2 |- (ps -> A.xps)
3		19.21adv.1	. 2 |- (ph -> (ps -> ch))
4	1, 2, 3	19.21ad 1406	1 |- (ph -> (ps -> A.xch))

Syntax hints:   -> wi 3  A.wal 1296

This theorem is referenced by:  zfpair 3522  ssrelOLD 4076  ssrelrelOLD 4084  funcnvuni 4482  eqfnfv 4766  cbvfo 4861  isofrlem 4878  f1oweALT 4883  tz7.49 5168  fodomfi 5656  ordtypelem4 5687  truniALT 5845  omsubsuc2 5878  aceq5lem4 5900  aceq5 5902  zorn2lem4 5953  zorn2lem7 5956  genpcl 6263  psslinpr 6287  prlem934 6291  ltaddpr 6292  ltexprlem3 6296  suplem1pr 6313  dfuzi 7414  uzwo4OLD 7422  uzwo 7624  uzwoOLD 7625  metcnp4 9248  gapm 9462  findcard 10178  findcardOLD 10179  fbssint 10279  fbunfip 10282  hausfillim 10303  inficlALT 15372  finsschain 15373  ordtypelem4OLD 15378  omsubsuc2OLD 15387  cncls 15419  cnntr 15420  alexsublem3 15439  cnconn 15444  neibastop3 15524  fcluscomplem 15620  findcard2 15745  frfi 15771  gen21 16514  gen22 16516  ggen22 16517

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

Copyright terms: Public domain