Theorem 19.21aivv 1287

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

Hypothesis

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

Assertion

Ref	Expression
19.21aivv	|- (ph -> A.xA.yps)

Distinct variable groups:   ph,x   ph,y

Proof of Theorem 19.21aivv

Step	Hyp	Ref	Expression
1		19.21aivv.1	. . 3 |- (ph -> ps)
2	1	19.21aiv 1286	. 2 |- (ph -> A.yps)
3	2	19.21aiv 1286	1 |- (ph -> A.xA.yps)

Syntax hints:   -> wi 3  A.wal 954

This theorem is referenced by:  csbiegf 2031  dfwe2 2935  ordelord 2970  relssdv 3249  cnvss 3291  iss 3397  cnvsym 3437  cores 3499  funssres 3552  funun 3554  fununi 3563  fn0 3605  fcoi1 3645  fcoi2 3646  fcnvres 3648  fnopabfv 3758  fsn 3834  dfoprab5 4115  th3qlem1 4314  inf3lem6 4618  zorn2lem6 4793  ubthlem4 8532  spwmo 8656  projlem28 9213  oefil2 10567  neifil 10568  filintf 10569  rcfpfil 10597  rcfpfilOLD 10598  sfvlim 10605

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

Copyright terms: Public domain