Theorem bnj1478 13154

Description: First-order logic and set theory.

Hypotheses

Ref	Expression
bnj1478.1	|- (ph -> A.xps)
bnj1478.2	|- (ps -> ch)

Assertion

Ref	Expression
bnj1478	|- (ph -> A.xch)

Proof of Theorem bnj1478

Step	Hyp	Ref	Expression
1		bnj1478.1	. 2 |- (ph -> A.xps)
2		bnj1478.2	. . 3 |- (ps -> ch)
3	2	alimi 1338	. 2 |- (A.xps -> A.xch)
4	1, 3	syl 12	1 |- (ph -> A.xch)

Syntax hints:   -> wi 3  A.wal 1296

This theorem is referenced by:  bnj1476 13156  bnj1532 13181  bnj1533 13182

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

Copyright terms: Public domain