Theorem 19.21aivv 944

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 group(s):   ph,x   ph,y

Proof of Theorem 19.21aivv

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

Syntax hints:   -> wi 2  A.wal 672

This theorem is referenced by:  dfwe2 2187  wereu 2197  ordelord 2221  relssdv 2482  cnvss 2512  iss 2599  cnvsym 2626  cores 2659  funssres 2698  funun 2700  fununi 2705  fn0 2739  fcoi1 2765  fcoi2 2766  fcnvres 2768  fnopabfv 2858  fsn 2895  th3qlem1 3250  inf3lem6 3469  zornlem6 3608  projlem28 5220

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925

metamath.org