Theorem hbal 1037

Description: If x is not free in ph, it is not free in A.yph.

Hypothesis

Ref	Expression
hb.1	|- (ph -> A.xph)

Assertion

Ref	Expression
hbal	|- (A.yph -> A.xA.yph)

Proof of Theorem hbal

Step	Hyp	Ref	Expression
1		hb.1	. . 3 |- (ph -> A.xph)
2	1	19.20i 1024	. 2 |- (A.yph -> A.yA.xph)
3		ax-7 994	. 2 |- (A.yA.xph -> A.xA.yph)
4	2, 3	syl 10	1 |- (A.yph -> A.xA.yph)

Syntax hints:   -> wi 3  A.wal 986

This theorem is referenced by:  hbex 1038  hba2 1045  aaan 1151  sb8 1294  cbval2 1349  euf 1417  mo 1426  2mo 1481  2eu3 1485  bm1.1 1498  hbeq 1602  hbral 1724  ralcom2 1814  moi 1963  uniiunlem 2176  hbint 2591  axrep1 2745  axrep2 2746  axrep3 2747  axrep4 2748  onminex 3075  dmcosseq 3425  axrepndlem1 5033  zfcndrep 5055  zfcndinf 5059  nnwof 6519

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-7 994  ax-gen 995  ax-4 1005  ax-5o 1007

Copyright terms: Public domain