Theorem 19.21ai 740

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

Hypotheses

Ref	Expression
19.21ai.1	|- (ph -> A.xph)
19.21ai.2	|- (ph -> ps)

Assertion

Ref	Expression
19.21ai	|- (ph -> A.xps)

Proof of Theorem 19.21ai

Step	Hyp	Ref	Expression
1		19.21ai.1	. 2 |- (ph -> A.xph)
2		19.21ai.2	. . 3 |- (ph -> ps)
3	2	19.20i 691	. 2 |- (A.xph -> A.xps)
4	1, 3	syl 12	1 |- (ph -> A.xps)

Syntax hints:   -> wi 2  A.wal 672

This theorem is referenced by:  19.21ad 741  19.22d 744  19.23 745  19.23ad 748  19.38 760  nexd 780  biald 782  biexd 783  hbnd 786  sb6x 871  bisbd 897  ddelimdf 909  sb5f1 917  sb8 918  a16g 933  19.21aiv 943  2moex 1060  biabd 1182  r19.21ai 1258  r19.15 1292  ceqsalg 1362  ceqsex 1370  zfrepclf 1477  ssopab2 2119  dmcosseq 2572  imadif 2714  fnopabg 2745  axrepnd 3740  axunnd 3742  axpownd 3747  axregndlem1 3748  axacndlem1 3753  axacndlem2 3754  axacndlem3 3755  axacndlem4 3756  axacndlem5 3757  axacnd 3758  suppsr3 4018  chcmh 5148

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

metamath.org