Theorem 19.21aivv 1282

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 1281	. 2 |- (ph -> A.yps)
3	2	19.21aiv 1281	1 |- (ph -> A.xA.yps)

Syntax hints:   -> wi 3  A.wal 951

This theorem is referenced by:  csbiegf 2021  dfwe2 2925  ordelord 2960  relssdv 3239  cnvss 3280  iss 3381  cnvsym 3421  cores 3485  funssres 3538  funun 3540  fununi 3549  fn0 3591  fcoi1 3630  fcoi2 3631  fcnvres 3633  fnopabfv 3743  fsn 3819  dfoprab5 4099  th3qlem1 4298  inf3lem6 4590  zorn2lem6 4765  ubthlem4 8463  spwmo 8580  projlem28 9129  oefil2 10441  neifil 10442  filintf 10443

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972

Copyright terms: Public domain